equal
deleted
inserted
replaced
595 end; |
595 end; |
596 val stmt_const = case Code.get_datatype_of_constr thy c |
596 val stmt_const = case Code.get_datatype_of_constr thy c |
597 of SOME tyco => stmt_datatypecons tyco |
597 of SOME tyco => stmt_datatypecons tyco |
598 | NONE => (case AxClass.class_of_param thy c |
598 | NONE => (case AxClass.class_of_param thy c |
599 of SOME class => stmt_classparam class |
599 of SOME class => stmt_classparam class |
600 | NONE => stmt_fun (Code_Funcgr.typ funcgr c, Code_Funcgr.eqns funcgr c)) |
600 | NONE => stmt_fun (Code_Wellsorted.typ funcgr c, Code_Wellsorted.eqns funcgr c)) |
601 in ensure_stmt lookup_const (declare_const thy) stmt_const c end |
601 in ensure_stmt lookup_const (declare_const thy) stmt_const c end |
602 and translate_term thy algbr funcgr thm (Const (c, ty)) = |
602 and translate_term thy algbr funcgr thm (Const (c, ty)) = |
603 translate_app thy algbr funcgr thm ((c, ty), []) |
603 translate_app thy algbr funcgr thm ((c, ty), []) |
604 | translate_term thy algbr funcgr thm (Free (v, _)) = |
604 | translate_term thy algbr funcgr thm (Free (v, _)) = |
605 pair (IVar v) |
605 pair (IVar v) |
620 ##>> fold_map (translate_term thy algbr funcgr thm) ts |
620 ##>> fold_map (translate_term thy algbr funcgr thm) ts |
621 #>> (fn (t, ts) => t `$$ ts) |
621 #>> (fn (t, ts) => t `$$ ts) |
622 and translate_const thy algbr funcgr thm (c, ty) = |
622 and translate_const thy algbr funcgr thm (c, ty) = |
623 let |
623 let |
624 val tys = Sign.const_typargs thy (c, ty); |
624 val tys = Sign.const_typargs thy (c, ty); |
625 val sorts = (map snd o fst o Code_Funcgr.typ funcgr) c; |
625 val sorts = (map snd o fst o Code_Wellsorted.typ funcgr) c; |
626 val tys_args = (fst o Term.strip_type) ty; |
626 val tys_args = (fst o Term.strip_type) ty; |
627 in |
627 in |
628 ensure_const thy algbr funcgr c |
628 ensure_const thy algbr funcgr c |
629 ##>> fold_map (translate_dicts thy algbr funcgr thm) (tys ~~ sorts) |
629 ##>> fold_map (translate_dicts thy algbr funcgr thm) (tys ~~ sorts) |
630 ##>> fold_map (translate_typ thy algbr funcgr) tys_args |
630 ##>> fold_map (translate_typ thy algbr funcgr) tys_args |
733 val cs_all = Graph.all_succs program cs; |
733 val cs_all = Graph.all_succs program cs; |
734 in (cs, (naming, Graph.subgraph (member (op =) cs_all) program)) end; |
734 in (cs, (naming, Graph.subgraph (member (op =) cs_all) program)) end; |
735 fun generate_consts thy algebra funcgr = |
735 fun generate_consts thy algebra funcgr = |
736 fold_map (ensure_const thy algebra funcgr); |
736 fold_map (ensure_const thy algebra funcgr); |
737 in |
737 in |
738 invoke_generation thy (Code_Funcgr.make thy cs) generate_consts cs |
738 invoke_generation thy (Code_Wellsorted.make thy cs) generate_consts cs |
739 |-> project_consts |
739 |-> project_consts |
740 end; |
740 end; |
741 |
741 |
742 |
742 |
743 (* value evaluation *) |
743 (* value evaluation *) |
776 val (((naming, program), (vs_ty_t, deps)), _) = |
776 val (((naming, program), (vs_ty_t, deps)), _) = |
777 invoke_generation thy (algebra, funcgr) ensure_value t'; |
777 invoke_generation thy (algebra, funcgr) ensure_value t'; |
778 in evaluator'' naming program vs_ty_t deps end; |
778 in evaluator'' naming program vs_ty_t deps end; |
779 in (t', evaluator') end |
779 in (t', evaluator') end |
780 |
780 |
781 fun eval_conv thy = Code_Funcgr.eval_conv thy o eval thy; |
781 fun eval_conv thy = Code_Wellsorted.eval_conv thy o eval thy; |
782 fun eval_term thy = Code_Funcgr.eval_term thy o eval thy; |
782 fun eval_term thy = Code_Wellsorted.eval_term thy o eval thy; |
783 |
783 |
784 end; (*struct*) |
784 end; (*struct*) |
785 |
785 |
786 |
786 |
787 structure Basic_Code_Thingol: BASIC_CODE_THINGOL = Code_Thingol; |
787 structure Basic_Code_Thingol: BASIC_CODE_THINGOL = Code_Thingol; |