From 7fdb587a1b1764459d2de2e789b30cb180fb172f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 2 Feb 2013 00:38:05 +0000 Subject: [PATCH] Implementation of Ocaml extraction (largely ported from Coq). Note: yet to be thoroughly debugged. In order to use, recompile everything with "OCAML_EXTRACTION=1 ocamlc". --- .../METAS/meta.helm-grafite_engine.src | 2 +- .../METAS/meta.helm-ng_extraction.src | 5 + matita/components/Makefile | 1 + .../grafite_engine/grafiteEngine.ml | 35 +- .../components/grafite_engine/grafiteTypes.ml | 1 + .../grafite_engine/grafiteTypes.mli | 1 + matita/components/ng_kernel/.depend | 7 - matita/components/ng_kernel/.depend.opt | 7 - matita/components/ng_kernel/Makefile | 3 +- matita/components/ng_kernel/nCicExtraction.ml | 1270 ----------------- .../components/ng_kernel/nCicExtraction.mli | 40 - matita/components/ng_library/nCicLibrary.mli | 2 +- matita/matita/matitaEngine.ml | 35 +- 13 files changed, 58 insertions(+), 1351 deletions(-) create mode 100644 matita/components/METAS/meta.helm-ng_extraction.src delete mode 100644 matita/components/ng_kernel/nCicExtraction.ml delete mode 100644 matita/components/ng_kernel/nCicExtraction.mli diff --git a/matita/components/METAS/meta.helm-grafite_engine.src b/matita/components/METAS/meta.helm-grafite_engine.src index 2362f2e6c..f770b0e0f 100644 --- a/matita/components/METAS/meta.helm-grafite_engine.src +++ b/matita/components/METAS/meta.helm-grafite_engine.src @@ -1,4 +1,4 @@ -requires="helm-library helm-grafite helm-ng_tactics helm-ng_library" +requires="helm-library helm-grafite helm-ng_tactics helm-ng_library helm-ng_extraction" version="0.0.1" archive(byte)="grafite_engine.cma" archive(native)="grafite_engine.cmxa" diff --git a/matita/components/METAS/meta.helm-ng_extraction.src b/matita/components/METAS/meta.helm-ng_extraction.src new file mode 100644 index 000000000..16e86f1fc --- /dev/null +++ b/matita/components/METAS/meta.helm-ng_extraction.src @@ -0,0 +1,5 @@ +requires="helm-ng_kernel helm-registry" +version="0.0.1" +archive(byte)="ng_extraction.cma" +archive(native)="ng_extraction.cmxa" +linkopts="" diff --git a/matita/components/Makefile b/matita/components/Makefile index 61ce8a364..f30f28434 100644 --- a/matita/components/Makefile +++ b/matita/components/Makefile @@ -13,6 +13,7 @@ MODULES = \ thread \ logger \ ng_kernel \ + ng_extraction \ getter \ library \ content \ diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 9fbcd9472..5828bdea1 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -286,6 +286,15 @@ let basic_extract_obj obj status = | exn -> prerr_endline ("EXTRACTION FAILURE: " ^ Printexc.to_string exn); assert false ;; +let basic_extract_ocaml_obj obj status = + try + let status = OcamlExtraction.print_ocaml_of_obj status obj in + let infos,status = status#get_info in + status,infos + with + exn -> prerr_endline ("EXTRACTION FAILURE: " ^ Printexc.to_string exn); assert false +;; + let inject_extract_obj = let basic_extract_obj info ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference @@ -298,11 +307,28 @@ let inject_extract_obj = GrafiteTypes.Serializer.register#run "extraction" basic_extract_obj ;; +let inject_extract_ocaml_obj = + let basic_extract_ocaml_obj info + ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference + ~alias_only status + = + let info= OcamlExtractionTable.refresh_uri_in_info ~refresh_uri_in_reference ~refresh_uri:NCicLibrary.refresh_uri info in + status#set_ocaml_extraction_db + (OcamlExtractionTable.register_infos status#ocaml_extraction_db info) + in + GrafiteTypes.Serializer.register#run "ocaml_extraction" basic_extract_ocaml_obj +;; + let eval_extract_obj status obj = let status,infos = basic_extract_obj obj status in NCicLibrary.dump_obj status (inject_extract_obj infos) ;; +let eval_extract_ocaml_obj status obj = + let status,infos = basic_extract_ocaml_obj obj status in + NCicLibrary.dump_obj status (inject_extract_ocaml_obj infos) +;; + (* module EmptyC = struct @@ -532,8 +558,11 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = let baseuri = NUri.uri_of_string baseuri in (* MATITA 1.0: keep WithoutPreferences? *) let alias_only = (mode = GrafiteAst.OnlyPreferences) in + let status = GrafiteTypes.Serializer.require - ~alias_only ~baseuri ~fname:fullpath status + ~alias_only ~baseuri ~fname:fullpath status in + OcamlExtraction.print_open status + (NCicLibrary.get_transitively_included status) | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n | GrafiteAst.NCoercion (loc, name, compose, None) -> let status, t, ty, source, target = @@ -611,6 +640,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = let old_status = status in let status = NCicLibrary.add_obj status obj in let status = eval_extract_obj status obj in + let status = eval_extract_ocaml_obj status obj in (try let index_obj = index && match obj_kind with @@ -782,7 +812,8 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = List.fold_left (fun status uri -> let obj = NCicEnvironment.get_checked_obj status uri in - eval_extract_obj status obj + let status = eval_extract_obj status obj in + eval_extract_ocaml_obj status obj ) status nuris in eval_alias status (mode,aliases) diff --git a/matita/components/grafite_engine/grafiteTypes.ml b/matita/components/grafite_engine/grafiteTypes.ml index 27a5cb61e..12935e80d 100644 --- a/matita/components/grafite_engine/grafiteTypes.ml +++ b/matita/components/grafite_engine/grafiteTypes.ml @@ -42,6 +42,7 @@ class virtual status = fun (b : string) -> inherit NCicLibrary.dumpable_status inherit NCicLibrary.status inherit NCicExtraction.status + inherit OcamlExtractionTable.status inherit GrafiteParser.status inherit TermContentPres.status val baseuri = b diff --git a/matita/components/grafite_engine/grafiteTypes.mli b/matita/components/grafite_engine/grafiteTypes.mli index 65cda299c..95e994350 100644 --- a/matita/components/grafite_engine/grafiteTypes.mli +++ b/matita/components/grafite_engine/grafiteTypes.mli @@ -39,6 +39,7 @@ class virtual status : inherit NCicLibrary.dumpable_status inherit NCicLibrary.status inherit NCicExtraction.status + inherit OcamlExtractionTable.status inherit GrafiteParser.status inherit TermContentPres.status method baseuri: string diff --git a/matita/components/ng_kernel/.depend b/matita/components/ng_kernel/.depend index 468f3d4b2..16f0d02cc 100644 --- a/matita/components/ng_kernel/.depend +++ b/matita/components/ng_kernel/.depend @@ -7,7 +7,6 @@ nCicReduction.cmi: nCic.cmo nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCic.cmo nCicUntrusted.cmi: nCic.cmo nCicPp.cmi: nReference.cmi nCic.cmo -nCicExtraction.cmi: nReference.cmi nCic.cmo nCic.cmo: nUri.cmi nReference.cmi nCic.cmx: nUri.cmx nReference.cmx nUri.cmo: nUri.cmi @@ -40,9 +39,3 @@ nCicPp.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCicReduction.cmi \ nCicEnvironment.cmi nCic.cmo nCicPp.cmi nCicPp.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \ nCicEnvironment.cmx nCic.cmx nCicPp.cmi -nCicExtraction.cmo: nUri.cmi nReference.cmi nCicUntrusted.cmi \ - nCicTypeChecker.cmi nCicSubstitution.cmi nCicReduction.cmi nCicPp.cmi \ - nCicEnvironment.cmi nCic.cmo nCicExtraction.cmi -nCicExtraction.cmx: nUri.cmx nReference.cmx nCicUntrusted.cmx \ - nCicTypeChecker.cmx nCicSubstitution.cmx nCicReduction.cmx nCicPp.cmx \ - nCicEnvironment.cmx nCic.cmx nCicExtraction.cmi diff --git a/matita/components/ng_kernel/.depend.opt b/matita/components/ng_kernel/.depend.opt index b5f0bb930..c57bf8efe 100644 --- a/matita/components/ng_kernel/.depend.opt +++ b/matita/components/ng_kernel/.depend.opt @@ -7,7 +7,6 @@ nCicReduction.cmi: nCic.cmx nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCic.cmx nCicUntrusted.cmi: nCic.cmx nCicPp.cmi: nReference.cmi nCic.cmx -nCicExtraction.cmi: nReference.cmi nCic.cmx nCic.cmo: nUri.cmi nReference.cmi nCic.cmx: nUri.cmx nReference.cmx nUri.cmo: nUri.cmi @@ -40,9 +39,3 @@ nCicPp.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCicReduction.cmi \ nCicEnvironment.cmi nCic.cmx nCicPp.cmi nCicPp.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \ nCicEnvironment.cmx nCic.cmx nCicPp.cmi -nCicExtraction.cmo: nUri.cmi nReference.cmi nCicUntrusted.cmi \ - nCicTypeChecker.cmi nCicSubstitution.cmi nCicReduction.cmi nCicPp.cmi \ - nCicEnvironment.cmi nCic.cmx nCicExtraction.cmi -nCicExtraction.cmx: nUri.cmx nReference.cmx nCicUntrusted.cmx \ - nCicTypeChecker.cmx nCicSubstitution.cmx nCicReduction.cmx nCicPp.cmx \ - nCicEnvironment.cmx nCic.cmx nCicExtraction.cmi diff --git a/matita/components/ng_kernel/Makefile b/matita/components/ng_kernel/Makefile index 6bca07465..35b89f3b1 100644 --- a/matita/components/ng_kernel/Makefile +++ b/matita/components/ng_kernel/Makefile @@ -10,8 +10,7 @@ INTERFACE_FILES = \ nCicReduction.mli \ nCicTypeChecker.mli \ nCicUntrusted.mli \ - nCicPp.mli \ - nCicExtraction.mli + nCicPp.mli IMPLEMENTATION_FILES = \ nCic.ml $(INTERFACE_FILES:%.mli=%.ml) diff --git a/matita/components/ng_kernel/nCicExtraction.ml b/matita/components/ng_kernel/nCicExtraction.ml deleted file mode 100644 index 4e167004d..000000000 --- a/matita/components/ng_kernel/nCicExtraction.ml +++ /dev/null @@ -1,1270 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* $Id: cicPp.ml 7413 2007-05-29 15:30:53Z tassi $ *) - -let fix_sorts t = t;; -let apply_subst subst t = assert (subst=[]); t;; - -type typformerreference = NReference.reference -type reference = NReference.reference - -type kind = - | Type - | KArrow of kind * kind - | KSkip of kind (* dropped abstraction *) - -let rec size_of_kind = - function - | Type -> 1 - | KArrow (l, r) -> 1 + size_of_kind l + size_of_kind r - | KSkip k -> size_of_kind k -;; - -let bracket ?(prec=1) size_of pp o = - if size_of o > prec then - "(" ^ pp o ^ ")" - else - pp o -;; - -let rec pretty_print_kind = - function - | Type -> "*" - | KArrow (l, r) -> bracket size_of_kind pretty_print_kind l ^ " -> " ^ pretty_print_kind r - | KSkip k -> pretty_print_kind k -;; - -type typ = - | Var of int - | Unit - | Top - | TConst of typformerreference - | Arrow of typ * typ - | TSkip of typ - | Forall of string * kind * typ - | TAppl of typ list - -let rec size_of_type = - function - | Var _ -> 0 - | Unit -> 0 - | Top -> 0 - | TConst _ -> 0 - | Arrow _ -> 2 - | TSkip t -> size_of_type t - | Forall _ -> 2 - | TAppl _ -> 1 -;; - -(* None = dropped abstraction *) -type typ_context = (string * kind) option list -type term_context = (string * [`OfKind of kind | `OfType of typ]) option list - -type typ_former_decl = typ_context * kind -type typ_former_def = typ_former_decl * typ - -type term = - | Rel of int - | UnitTerm - | Const of reference - | Lambda of string * (* typ **) term - | Appl of term list - | LetIn of string * (* typ **) term * term - | Match of reference * term * (term_context * term) list - | BottomElim - | TLambda of string * term - | Inst of (*typ_former **) term - | Skip of term - | UnsafeCoerce of term -;; - -type term_former_decl = term_context * typ -type term_former_def = term_former_decl * term - -let mk_appl f x = - match f with - Appl args -> Appl (args@[x]) - | _ -> Appl [f;x] - -let mk_tappl f l = - match f with - TAppl args -> TAppl (args@l) - | _ -> TAppl (f::l) - -let rec size_of_term = - function - | Rel _ -> 1 - | UnitTerm -> 1 - | Const _ -> 1 - | Lambda (_, body) -> 1 + size_of_term body - | Appl l -> List.length l - | LetIn (_, def, body) -> 1 + size_of_term def + size_of_term body - | Match (_, case, pats) -> 1 + size_of_term case + List.length pats - | BottomElim -> 1 - | TLambda (_,t) -> size_of_term t - | Inst t -> size_of_term t - | Skip t -> size_of_term t - | UnsafeCoerce t -> 1 + size_of_term t -;; - -module ReferenceMap = Map.Make(struct type t = NReference.reference let compare = NReference.compare end) - -module GlobalNames = Set.Make(String) - -type info_el = - string * [`Type of typ_context * typ option | `Constructor of typ | `Function of typ ] -type info = (NReference.reference * info_el) list -type db = info_el ReferenceMap.t * GlobalNames.t - -let empty_info = [] - -type obj_kind = - TypeDeclaration of typ_former_decl - | TypeDefinition of typ_former_def - | TermDeclaration of term_former_decl - | TermDefinition of term_former_def - | LetRec of (info * NReference.reference * obj_kind) list - (* reference, left, right, constructors *) - | Algebraic of (info * NReference.reference * typ_context * typ_context * (NReference.reference * typ) list) list - -type obj = info * NReference.reference * obj_kind - -(* For LetRec and Algebraic blocks *) -let dummyref = - NReference.reference_of_string "cic:/matita/dummy/dummy.ind(1,1,1)" - -type not_term = [`Kind | `KindOrType | `PropKind | `Proposition | `Type];; - -let max_not_term t1 t2 = - match t1,t2 with - `KindOrType,_ - | _,`KindOrType -> `KindOrType - | `Kind,_ - | _,`Kind -> `Kind - | `Type,_ - | _,`Type -> `Type - | `PropKind,_ - | _,`PropKind -> `PropKind - | `Proposition,`Proposition -> `Proposition - -let sup = List.fold_left max_not_term `Proposition - -let rec classify_not_term status context t = - match NCicReduction.whd status ~subst:[] context t with - | NCic.Sort s -> - (match s with - NCic.Prop - | NCic.Type [`CProp,_] -> `PropKind - | NCic.Type [`Type,_] -> `Kind - | NCic.Type _ -> assert false) - | NCic.Prod (b,s,t) -> - (*CSC: using invariant on "_" *) - classify_not_term status ((b,NCic.Decl s)::context) t - | NCic.Implicit _ - | NCic.LetIn _ - | NCic.Const (NReference.Ref (_,NReference.CoFix _)) - | NCic.Appl [] -> - assert false (* NOT POSSIBLE *) - | NCic.Lambda (n,s,t) -> - (* Lambdas can me met in branches of matches, expecially when the - output type is a product *) - classify_not_term status ((n,NCic.Decl s)::context) t - | NCic.Match (_,_,_,pl) -> - let classified_pl = List.map (classify_not_term status context) pl in - sup classified_pl - | NCic.Const (NReference.Ref (_,NReference.Fix _)) -> - assert false (* IMPOSSIBLE *) - | NCic.Meta _ -> assert false (* TODO *) - | NCic.Appl (NCic.Const (NReference.Ref (_,NReference.Fix (i,_,_)) as r)::_)-> - let l,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes status r in - let _,_,_,_,bo = List.nth l i in - classify_not_term status [] bo - | NCic.Appl (he::_) -> classify_not_term status context he - | NCic.Rel n -> - let rec find_sort typ = - match NCicReduction.whd status ~subst:[] context (NCicSubstitution.lift status n typ) with - NCic.Sort NCic.Prop -> `Proposition - | NCic.Sort (NCic.Type [`CProp,_]) -> `Proposition - | NCic.Sort (NCic.Type [`Type,_]) -> - (*CSC: we could be more precise distinguishing the user provided - minimal elements of the hierarchies and classify these - as `Kind *) - `KindOrType - | NCic.Sort (NCic.Type _) -> assert false (* ALGEBRAIC *) - | NCic.Prod (_,_,t) -> - (* we skipped arguments of applications, so here we need to skip - products *) - find_sort t - | _ -> assert false (* NOT A SORT *) - in - (match List.nth context (n-1) with - _,NCic.Decl typ -> find_sort typ - | _,NCic.Def _ -> assert false (* IMPOSSIBLE *)) - | NCic.Const (NReference.Ref (_,NReference.Decl) as ref) -> - let _,_,ty,_,_ = NCicEnvironment.get_checked_decl status ref in - (match classify_not_term status [] ty with - | `Proposition - | `Type -> assert false (* IMPOSSIBLE *) - | `Kind - | `KindOrType -> `Type - | `PropKind -> `Proposition) - | NCic.Const (NReference.Ref (_,NReference.Ind _) as ref) -> - let _,_,ityl,_,i = NCicEnvironment.get_checked_indtys status ref in - let _,_,arity,_ = List.nth ityl i in - (match classify_not_term status [] arity with - | `Proposition - | `Type - | `KindOrType -> assert false (* IMPOSSIBLE *) - | `Kind -> `Type - | `PropKind -> `Proposition) - | NCic.Const (NReference.Ref (_,NReference.Con _)) - | NCic.Const (NReference.Ref (_,NReference.Def _)) -> - assert false (* IMPOSSIBLE *) -;; - -let classify status ~metasenv context t = - match NCicTypeChecker.typeof status ~metasenv ~subst:[] context t with - | NCic.Sort _ -> - (classify_not_term status context t : not_term :> [> not_term]) - | ty -> - let ty = fix_sorts ty in - `Term - (match classify_not_term status context ty with - | `Proposition -> `Proof - | `Type -> `Term - | `KindOrType -> `TypeFormerOrTerm - | `Kind -> `TypeFormer - | `PropKind -> `PropFormer) -;; - - -let rec kind_of status ~metasenv context k = - match NCicReduction.whd status ~subst:[] context k with - | NCic.Sort NCic.Type _ -> Type - | NCic.Sort _ -> assert false (* NOT A KIND *) - | NCic.Prod (b,s,t) -> - (match classify status ~metasenv context s with - | `Kind -> - KArrow (kind_of status ~metasenv context s, - kind_of ~metasenv status ((b,NCic.Decl s)::context) t) - | `Type - | `KindOrType - | `Proposition - | `PropKind -> - KSkip (kind_of status ~metasenv ((b,NCic.Decl s)::context) t) - | `Term _ -> assert false (* IMPOSSIBLE *)) - | NCic.Implicit _ - | NCic.LetIn _ -> assert false (* IMPOSSIBLE *) - | NCic.Lambda _ - | NCic.Rel _ - | NCic.Const _ -> assert false (* NOT A KIND *) - | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec; - otherwise NOT A KIND *) - | NCic.Meta _ - | NCic.Match (_,_,_,_) -> assert false (* TODO *) -;; - -let rec skip_args status ~metasenv context = - function - | _,[] -> [] - | [],_ -> assert false (* IMPOSSIBLE *) - | None::tl1,_::tl2 -> skip_args status ~metasenv context (tl1,tl2) - | _::tl1,arg::tl2 -> - match classify status ~metasenv context arg with - | `KindOrType - | `Type - | `Term `TypeFormer -> - Some arg::skip_args status ~metasenv context (tl1,tl2) - | `Kind - | `Proposition - | `PropKind -> None::skip_args status ~metasenv context (tl1,tl2) - | `Term _ -> assert false (* IMPOSSIBLE *) -;; - -class type g_status = - object - method extraction_db: db - end - -class virtual status = - object - inherit NCic.status - val extraction_db = ReferenceMap.empty, GlobalNames.empty - method extraction_db = extraction_db - method set_extraction_db v = {< extraction_db = v >} - method set_extraction_status - : 'status. #g_status as 'status -> 'self - = fun o -> {< extraction_db = o#extraction_db >} - end - -let xdo_pretty_print_type = ref (fun _ _ -> assert false) -let do_pretty_print_type status ctx t = - !xdo_pretty_print_type (status : #status :> status) ctx t - -let xdo_pretty_print_term = ref (fun _ _ -> assert false) -let do_pretty_print_term status ctx t = - !xdo_pretty_print_term (status : #status :> status) ctx t - -let term_ctx_of_type_ctx = - List.map - (function - None -> None - | Some (name,k) -> Some (name,`OfKind k)) - -let rec split_kind_prods context = - function - | KArrow (so,ta)-> split_kind_prods (Some ("_",so)::context) ta - | KSkip ta -> split_kind_prods (None::context) ta - | Type -> context,Type -;; - -let rec split_typ_prods context = - function - | Arrow (so,ta)-> split_typ_prods (Some ("_",`OfType so)::context) ta - | Forall (name,so,ta)-> split_typ_prods (Some (name,`OfKind so)::context) ta - | TSkip ta -> split_typ_prods (None::context) ta - | _ as t -> context,t -;; - -let rec glue_ctx_typ ctx typ = - match ctx with - | [] -> typ - | Some (_,`OfType so)::ctx -> glue_ctx_typ ctx (Arrow (so,typ)) - | Some (name,`OfKind so)::ctx -> glue_ctx_typ ctx (Forall (name,so,typ)) - | None::ctx -> glue_ctx_typ ctx (TSkip typ) -;; - -let rec split_typ_lambdas status n ~metasenv context typ = - if n = 0 then context,typ - else - match NCicReduction.whd status ~delta:max_int ~subst:[] context typ with - | NCic.Lambda (name,s,t) -> - split_typ_lambdas status (n-1) ~metasenv ((name,NCic.Decl s)::context) t - | t -> - (* eta-expansion required *) - let ty = NCicTypeChecker.typeof status ~metasenv ~subst:[] context t in - match NCicReduction.whd status ~delta:max_int ~subst:[] context ty with - | NCic.Prod (name,typ,_) -> - split_typ_lambdas status (n-1) ~metasenv - ((name,NCic.Decl typ)::context) - (NCicUntrusted.mk_appl t [NCic.Rel 1]) - | _ -> assert false (* IMPOSSIBLE *) -;; - - -let rev_context_of_typformer status ~metasenv context = - function - NCic.Const (NReference.Ref (_,NReference.Ind _) as ref) - | NCic.Const (NReference.Ref (_,NReference.Def _) as ref) - | NCic.Const (NReference.Ref (_,NReference.Decl) as ref) - | NCic.Const (NReference.Ref (_,NReference.Fix _) as ref) -> - (try - match snd (ReferenceMap.find ref (fst status#extraction_db)) with - `Type (ctx,_) -> List.rev ctx - | `Constructor _ - | `Function _ -> assert false - with - Not_found -> - (* This can happen only when we are processing the type of - the constructor of a small singleton type. In this case - we are not interested in all the type, but only in its - backbone. That is why we can safely return the dummy context - here *) - let rec dummy = None::dummy in - dummy) - | NCic.Match _ -> assert false (* TODO ???? *) - | NCic.Rel n -> - let typ = - match List.nth context (n-1) with - _,NCic.Decl typ -> typ - | _,NCic.Def _ -> assert false (* IMPOSSIBLE *) in - let typ_ctx = snd (HExtlib.split_nth n context) in - let typ = kind_of status ~metasenv typ_ctx typ in - List.rev (fst (split_kind_prods [] typ)) - | NCic.Meta _ -> assert false (* TODO *) - | NCic.Const (NReference.Ref (_,NReference.Con _)) - | NCic.Const (NReference.Ref (_,NReference.CoFix _)) - | NCic.Sort _ | NCic.Implicit _ | NCic.Lambda _ | NCic.LetIn _ - | NCic.Appl _ | NCic.Prod _ -> - assert false (* IMPOSSIBLE *) - -let rec typ_of status ~metasenv context k = - match NCicReduction.whd status ~delta:max_int ~subst:[] context k with - | NCic.Prod (b,s,t) -> - (* CSC: non-invariant assumed here about "_" *) - (match classify status ~metasenv context s with - | `Kind -> - Forall (b, kind_of status ~metasenv context s, - typ_of ~metasenv status ((b,NCic.Decl s)::context) t) - | `Type - | `KindOrType -> (* ??? *) - Arrow (typ_of status ~metasenv context s, - typ_of status ~metasenv ((b,NCic.Decl s)::context) t) - | `PropKind - | `Proposition -> - TSkip (typ_of status ~metasenv ((b,NCic.Decl s)::context) t) - | `Term _ -> assert false (* IMPOSSIBLE *)) - | NCic.Sort _ - | NCic.Implicit _ - | NCic.LetIn _ -> assert false (* IMPOSSIBLE *) - | NCic.Lambda _ -> Top (*assert false (* LAMBDA-LIFT INNER DECLARATION *)*) - | NCic.Rel n -> Var n - | NCic.Const ref -> TConst ref - | NCic.Match (_,_,_,_) - | NCic.Appl (NCic.Const (NReference.Ref (_,NReference.Fix _))::_) -> - Top - | NCic.Appl (he::args) -> - let rev_he_context= rev_context_of_typformer status ~metasenv context he in - TAppl (typ_of status ~metasenv context he :: - List.map - (function None -> Unit | Some ty -> typ_of status ~metasenv context ty) - (skip_args status ~metasenv context (rev_he_context,args))) - | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec; - otherwise NOT A TYPE *) - | NCic.Meta _ -> assert false (*TODO*) -;; - -let rec fomega_lift_type_from n k = - function - | Var m as t -> if m < k then t else Var (m + n) - | Top -> Top - | TConst _ as t -> t - | Unit -> Unit - | Arrow (ty1,ty2) -> Arrow (fomega_lift_type_from n k ty1,fomega_lift_type_from n (k+1) ty2) - | TSkip t -> TSkip (fomega_lift_type_from n (k+1) t) - | Forall (name,kind,t) -> Forall (name,kind,fomega_lift_type_from n (k+1) t) - | TAppl args -> TAppl (List.map (fomega_lift_type_from n k) args) - -let fomega_lift_type n t = - if n = 0 then t else fomega_lift_type_from n 0 t - -let fomega_lift_term n t = - let rec fomega_lift_term n k = - function - | Rel m as t -> if m < k then t else Rel (m + n) - | BottomElim - | UnitTerm - | Const _ as t -> t - | Lambda (name,t) -> Lambda (name,fomega_lift_term n (k+1) t) - | TLambda (name,t) -> TLambda (name,fomega_lift_term n (k+1) t) - | Appl args -> Appl (List.map (fomega_lift_term n k) args) - | LetIn (name,m,bo) -> - LetIn (name, fomega_lift_term n k m, fomega_lift_term n (k+1) bo) - | Match (ref,t,pl) -> - let lift_p (ctx,t) = - let lift_context ctx = - let len = List.length ctx in - HExtlib.list_mapi - (fun el i -> - let j = len - i - 1 in - match el with - None - | Some (_,`OfKind _) as el -> el - | Some (name,`OfType t) -> - Some (name,`OfType (fomega_lift_type_from n (k+j) t)) - ) ctx - in - lift_context ctx, fomega_lift_term n (k + List.length ctx) t - in - Match (ref,fomega_lift_term n k t,List.map lift_p pl) - | Inst t -> Inst (fomega_lift_term n k t) - | Skip t -> Skip (fomega_lift_term n (k+1) t) - | UnsafeCoerce t -> UnsafeCoerce (fomega_lift_term n k t) - in - if n = 0 then t else fomega_lift_term n 0 t -;; - -let rec fomega_subst k t1 = - function - | Var n -> - if k=n then fomega_lift_type (k-1) t1 - else if n < k then Var n - else Var (n-1) - | Top -> Top - | TConst ref -> TConst ref - | Unit -> Unit - | Arrow (ty1,ty2) -> Arrow (fomega_subst k t1 ty1, fomega_subst (k+1) t1 ty2) - | TSkip t -> TSkip (fomega_subst (k+1) t1 t) - | Forall (n,kind,t) -> Forall (n,kind,fomega_subst (k+1) t1 t) - | TAppl (he::args) -> - mk_tappl (fomega_subst k t1 he) (List.map (fomega_subst k t1) args) - | TAppl [] -> assert false - -let fomega_lookup status ref = - try - match snd (ReferenceMap.find ref (fst status#extraction_db)) with - `Type (_,bo) -> bo - | `Constructor _ - | `Function _ -> assert false - with - Not_found -> -prerr_endline ("BUG, THIS SHOULD NEVER HAPPEN " ^ NReference.string_of_reference ref); None - -let rec fomega_whd status ty = - match ty with - | TConst r -> - (match fomega_lookup status r with - None -> ty - | Some ty -> fomega_whd status ty) - | TAppl (TConst r::args) -> - (match fomega_lookup status r with - None -> ty - | Some ty -> fomega_whd status (List.fold_right (fomega_subst 1) args ty)) - | _ -> ty - -let rec fomega_conv_kind k1 k2 = - match k1,k2 with - Type,Type -> true - | KArrow (s1,t1), KArrow (s2,t2) -> - fomega_conv_kind s1 s2 && fomega_conv_kind t1 t2 - | KSkip k1, KSkip k2 -> fomega_conv_kind k1 k2 - | _,_ -> false - -let rec fomega_conv status t1 t2 = - match fomega_whd status t1, fomega_whd status t2 with - Var n, Var m -> n=m - | Unit, Unit -> true - | Top, Top -> true - | TConst r1, TConst r2 -> NReference.eq r1 r2 - | Arrow (s1,t1), Arrow (s2,t2) -> - fomega_conv status s1 s2 && fomega_conv status t1 t2 - | TSkip t1, TSkip t2 -> fomega_conv status t1 t2 - | Forall (_,k1,t1), Forall (_,k2,t2) -> - fomega_conv_kind k1 k2 && fomega_conv status t1 t2 - | TAppl tl1, TAppl tl2 -> - (try - List.fold_left2 (fun b t1 t2 -> b && fomega_conv status t1 t2) - true tl1 tl2 - with - Invalid_argument _ -> false) - | _,_ -> false - -exception PatchMe (* BUG: constructor of singleton type :-( *) - -let type_of_constructor status ref = - try - match snd (ReferenceMap.find ref (fst status#extraction_db)) with - `Constructor ty -> ty - | _ -> assert false - with - Not_found -> raise PatchMe (* BUG: constructor of singleton type :-( *) - -let type_of_appl_he status ~metasenv context = - function - NCic.Const (NReference.Ref (_,NReference.Con _) as ref) - | NCic.Const (NReference.Ref (_,NReference.Def _) as ref) - | NCic.Const (NReference.Ref (_,NReference.Decl) as ref) - | NCic.Const (NReference.Ref (_,NReference.Fix _) as ref) - | NCic.Const (NReference.Ref (_,NReference.CoFix _) as ref) -> - (try - match snd (ReferenceMap.find ref (fst status#extraction_db)) with - `Type _ -> assert false - | `Constructor ty - | `Function ty -> ty - with - Not_found -> assert false) - | NCic.Const (NReference.Ref (_,NReference.Ind _)) -> - assert false (* IMPOSSIBLE *) - | NCic.Rel n -> - (match List.nth context (n-1) with - _,NCic.Decl typ - | _,NCic.Def (_,typ) -> - (* recomputed every time *) - typ_of status ~metasenv context - (NCicSubstitution.lift status n typ)) - | (NCic.Lambda _ - | NCic.LetIn _ - | NCic.Match _) as t -> - (* BUG: here we should implement a real type-checker since we are - trusting the translation of the Cic one that could be wrong - (e.g. pruned abstractions, etc.) *) - (typ_of status ~metasenv context - (NCicTypeChecker.typeof status ~metasenv ~subst:[] context t)) - | NCic.Meta _ -> assert false (* TODO *) - | NCic.Sort _ | NCic.Implicit _ | NCic.Appl _ | NCic.Prod _ -> - assert false (* IMPOSSIBLE *) - -let rec term_of status ~metasenv context = - function - | NCic.Implicit _ - | NCic.Sort _ - | NCic.Prod _ -> assert false (* IMPOSSIBLE *) - | NCic.Lambda (b,ty,bo) -> - (* CSC: non-invariant assumed here about "_" *) - (match classify status ~metasenv context ty with - | `Kind -> - TLambda (b,term_of status ~metasenv ((b,NCic.Decl ty)::context) bo) - | `KindOrType (* ??? *) - | `Type -> - Lambda (b, term_of status ~metasenv ((b,NCic.Decl ty)::context) bo) - | `PropKind - | `Proposition -> - (* CSC: LAZY ??? *) - Skip (term_of status ~metasenv ((b,NCic.Decl ty)::context) bo) - | `Term _ -> assert false (* IMPOSSIBLE *)) - | NCic.LetIn (b,ty,t,bo) -> - (match classify status ~metasenv context t with - | `Term `TypeFormerOrTerm (* ???? *) - | `Term `Term -> - LetIn (b,term_of status ~metasenv context t, - term_of status ~metasenv ((b,NCic.Def (t,ty))::context) bo) - | `Kind - | `Type - | `KindOrType - | `PropKind - | `Proposition - | `Term `PropFormer - | `Term `TypeFormer - | `Term `Proof -> - (* not in programming languages, we expand it *) - term_of status ~metasenv context - (NCicSubstitution.subst status ~avoid_beta_redexes:true t bo)) - | NCic.Rel n -> Rel n - | NCic.Const ref -> Const ref - | NCic.Appl (he::args) -> - let hety = type_of_appl_he status ~metasenv context he in - eat_args status metasenv (term_of status ~metasenv context he) context - hety args - | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec; - otherwise NOT A TYPE *) - | NCic.Meta _ -> assert false (* TODO *) - | NCic.Match (ref,_,t,pl) -> - let patterns_of pl = - let _,leftno,_,_,_ = NCicEnvironment.get_checked_indtys status ref in - let rec eat_branch n ty context ctx pat = - match (ty, pat) with - | TSkip t,_ - | Forall (_,_,t),_ - | Arrow (_, t), _ when n > 0 -> - eat_branch (pred n) t context ctx pat - | _, _ when n > 0 -> assert false (*BUG: is Top possible here?*) - (*CSC: unify the three cases below? *) - | Arrow (_, t), NCic.Lambda (name, ty, t') -> - let ctx = - (Some (name,`OfType (typ_of status ~metasenv context ty)))::ctx in - let context = (name,NCic.Decl ty)::context in - eat_branch 0 t context ctx t' - | Forall (_,_,t),NCic.Lambda (name, ty, t') -> - let ctx = - (Some (name,`OfKind (kind_of status ~metasenv context ty)))::ctx in - let context = (name,NCic.Decl ty)::context in - eat_branch 0 t context ctx t' - | TSkip t,NCic.Lambda (name, ty, t') -> - let ctx = None::ctx in - let context = (name,NCic.Decl ty)::context in - eat_branch 0 t context ctx t' - | Top,_ -> assert false (* IMPOSSIBLE *) - | TSkip _, _ - | Forall _,_ - | Arrow _,_ -> assert false (*BUG here, eta-expand!*) - | _, _ -> context,ctx, pat - in - try - HExtlib.list_mapi - (fun pat i -> - let ref = NReference.mk_constructor (i+1) ref in - let ty = - (* BUG HERE, QUICK BUG WRONG PATCH IN PLACE *) - try - type_of_constructor status ref - with - PatchMe -> - typ_of status ~metasenv context - (NCicTypeChecker.typeof status ~metasenv ~subst:[] context - (NCic.Const ref)) - in - let context,lhs,rhs = eat_branch leftno ty context [] pat in - let rhs = - (* UnsafeCoerce not always required *) - UnsafeCoerce (term_of status ~metasenv context rhs) - in - lhs,rhs - ) pl - with Invalid_argument _ -> assert false - in - (match classify_not_term status [] (NCic.Const ref) with - | `PropKind - | `KindOrType - | `Kind -> assert false (* IMPOSSIBLE *) - | `Proposition -> - (match patterns_of pl with - [] -> BottomElim - | [lhs,rhs] -> fomega_lift_term (- List.length lhs) rhs - | _ -> assert false) - | `Type -> - Match (ref,term_of status ~metasenv context t, patterns_of pl)) -and eat_args status metasenv acc context tyhe = - function - [] -> acc - | arg::tl -> - match fomega_whd status tyhe with - Arrow (s,t) -> - let acc = - match s with - Unit -> mk_appl acc UnitTerm - | _ -> - let foarg = term_of status ~metasenv context arg in - (* BUG HERE, we should implement a real type-checker instead of - trusting the Cic type *) - let inferredty = - typ_of status ~metasenv context - (NCicTypeChecker.typeof status ~metasenv ~subst:[] context arg)in - if fomega_conv status inferredty s then - mk_appl acc foarg - else -( -prerr_endline ("ARG = " ^ status#ppterm ~metasenv ~subst:[] ~context arg); -let context = List.map fst context in -prerr_endline ("HE = " ^ do_pretty_print_term status context acc); -prerr_endline ("CONTEXT= " ^ String.concat " " context); -prerr_endline ("NOT CONV: " ^ do_pretty_print_type status context inferredty ^ " vs " ^ do_pretty_print_type status context s); - mk_appl acc (UnsafeCoerce foarg) -) - in - eat_args status metasenv acc context (fomega_subst 1 Unit t) tl - | Top -> - let arg = - match classify status ~metasenv context arg with - | `PropKind - | `Proposition - | `Term `TypeFormer - | `Term `PropFormer - | `Term `Proof - | `Type - | `KindOrType - | `Kind -> UnitTerm - | `Term `TypeFormerOrTerm - | `Term `Term -> term_of status ~metasenv context arg - in - (* BUG: what if an argument of Top has been erased??? *) - eat_args status metasenv - (UnsafeCoerce (mk_appl acc (UnsafeCoerce arg))) - context Top tl - | Forall (_,_,t) -> -(* -prerr_endline "FORALL"; -let xcontext = List.map fst context in -prerr_endline ("TYPE: " ^ do_pretty_print_type status xcontext (fomega_whd status tyhe)); -prerr_endline ("fARG = " ^ status#ppterm ~metasenv ~subst:[] ~context arg); -prerr_endline ("fHE = " ^ do_pretty_print_term status xcontext acc); -prerr_endline ("fCONTEXT= " ^ String.concat " " xcontext); -*) - (match classify status ~metasenv context arg with - | `PropKind -> assert false (*TODO: same as below, coercion needed???*) - | `Proposition - | `Kind -> - eat_args status metasenv (UnsafeCoerce (Inst acc)) - context (fomega_subst 1 Unit t) tl - | `KindOrType - | `Term `TypeFormer - | `Type -> - eat_args status metasenv (Inst acc) - context (fomega_subst 1 (typ_of status ~metasenv context arg) t) - tl - | `Term _ -> assert false (*TODO: ????*)) - | TSkip t -> - eat_args status metasenv acc context t tl - | Unit | Var _ | TConst _ | TAppl _ -> assert false (* NOT A PRODUCT *) -;; - -type 'a result = - | Erased - | OutsideTheory - | Failure of string - | Success of 'a -;; - -let fresh_name_of_ref status ref = - (*CSC: Patch while we wait for separate compilation *) - let candidate = - let name = NCicPp.r2s status true ref in - let NReference.Ref (uri,_) = ref in - let path = NUri.baseuri_of_uri uri in - let path = String.sub path 5 (String.length path - 5) in - let path = Str.global_replace (Str.regexp "/") "_" path in - path ^ "_" ^ name - in - let rec freshen candidate = - if GlobalNames.mem candidate (snd status#extraction_db) then - freshen (candidate ^ "'") - else - candidate - in - freshen candidate - -let register_info (db,names) (ref,(name,_ as info_el)) = - ReferenceMap.add ref info_el db,GlobalNames.add name names - -let register_name_and_info status (ref,info_el) = - let name = fresh_name_of_ref status ref in - let info = ref,(name,info_el) in - let infos,names = status#extraction_db in - status#set_extraction_db (register_info (infos,names) info), info - -let register_infos = List.fold_left register_info - -let object_of_constant status ~metasenv ref bo ty = - match classify status ~metasenv [] ty with - | `Kind -> - let ty = kind_of status ~metasenv [] ty in - let ctx0,res = split_kind_prods [] ty in - let ctx,bo = - split_typ_lambdas status ~metasenv (List.length ctx0) [] bo in - (match classify status ~metasenv ctx bo with - | `Type - | `KindOrType -> (* ?? no kind formers in System F_omega *) - let nicectx = - List.map2 - (fun p1 n -> - HExtlib.map_option (fun (_,k) -> - (*CSC: BUG here, clashes*) - String.uncapitalize (fst n),k) p1) - ctx0 ctx - in - let bo = typ_of status ~metasenv ctx bo in - let info = ref,`Type (nicectx,Some bo) in - let status,info = register_name_and_info status info in - status,Success ([info],ref,TypeDefinition((nicectx,res),bo)) - | `Kind -> status, Erased (* DPM: but not really, more a failure! *) - | `PropKind - | `Proposition -> status, Erased - | `Term _ -> status, Failure "Body of type lambda classified as a term. This is a bug.") - | `PropKind - | `Proposition -> status, Erased - | `KindOrType (* ??? *) - | `Type -> - let ty = typ_of status ~metasenv [] ty in - let info = ref,`Function ty in - let status,info = register_name_and_info status info in - status, - Success ([info],ref, TermDefinition (split_typ_prods [] ty, - term_of status ~metasenv [] bo)) - | `Term _ -> status, Failure "Non-term classified as a term. This is a bug." -;; - -let object_of_inductive status ~metasenv uri ind leftno il = - let status,_,rev_tyl = - List.fold_left - (fun (status,i,res) (_,_,arity,cl) -> - match classify_not_term status [] arity with - | `Proposition - | `KindOrType - | `Type -> assert false (* IMPOSSIBLE *) - | `PropKind -> status,i+1,res - | `Kind -> - let arity = kind_of status ~metasenv [] arity in - let ctx,_ = split_kind_prods [] arity in - let right,left = HExtlib.split_nth (List.length ctx - leftno) ctx in - let ref = - NReference.reference_of_spec uri (NReference.Ind (ind,i,leftno)) in - let info = ref,`Type (ctx,None) in - let status,info = register_name_and_info status info in - let _,status,cl_rev,infos = - List.fold_left - (fun (j,status,res,infos) (_,_,ty) -> - let ctx,ty = - NCicReduction.split_prods status ~subst:[] [] leftno ty in - let ty = typ_of status ~metasenv ctx ty in - let left = term_ctx_of_type_ctx left in - let full_ty = glue_ctx_typ left ty in - let ref = NReference.mk_constructor j ref in - let info = ref,`Constructor full_ty in - let status,info = register_name_and_info status info in - j+1,status,((ref,ty)::res),info::infos - ) (1,status,[],[]) cl - in - status,i+1,(info::infos,ref,left,right,List.rev cl_rev)::res - ) (status,0,[]) il - in - match rev_tyl with - [] -> status,Erased - | _ -> status, Success ([], dummyref, Algebraic (List.rev rev_tyl)) -;; - -let object_of status (uri,height,metasenv,subst,obj_kind) = - let obj_kind = apply_subst subst obj_kind in - match obj_kind with - | NCic.Constant (_,_,None,ty,_) -> - let ref = NReference.reference_of_spec uri NReference.Decl in - (match classify status ~metasenv [] ty with - | `Kind -> - let ty = kind_of status ~metasenv [] ty in - let ctx,_ as res = split_kind_prods [] ty in - let info = ref,`Type (ctx,None) in - let status,info = register_name_and_info status info in - status, Success ([info],ref, TypeDeclaration res) - | `PropKind - | `Proposition -> status, Erased - | `Type - | `KindOrType (*???*) -> - let ty = typ_of status ~metasenv [] ty in - let info = ref,`Function ty in - let status,info = register_name_and_info status info in - status,Success ([info],ref, - TermDeclaration (split_typ_prods [] ty)) - | `Term _ -> status, Failure "Type classified as a term. This is a bug.") - | NCic.Constant (_,_,Some bo,ty,_) -> - let ref = NReference.reference_of_spec uri (NReference.Def height) in - object_of_constant status ~metasenv ref bo ty - | NCic.Fixpoint (fix_or_cofix,fs,_) -> - let _,status,objs = - List.fold_right - (fun (_,_name,recno,ty,bo) (i,status,res) -> - let ref = - if fix_or_cofix then - NReference.reference_of_spec - uri (NReference.Fix (i,recno,height)) - else - NReference.reference_of_spec uri (NReference.CoFix i) - in - let status,obj = object_of_constant ~metasenv status ref bo ty in - match obj with - | Success (info,ref,obj) -> i+1,status, (info,ref,obj)::res - | _ -> i+1,status, res) fs (0,status,[]) - in - status, Success ([],dummyref,LetRec objs) - | NCic.Inductive (ind,leftno,il,_) -> - object_of_inductive status ~metasenv uri ind leftno il - -(************************ HASKELL *************************) - -(* ----------------------------------------------------------------------------- - * Helper functions I can't seem to find anywhere in the OCaml stdlib? - * ----------------------------------------------------------------------------- - *) -let (|>) f g = - fun x -> g (f x) -;; - -let curry f x y = - f (x, y) -;; - -let uncurry f (x, y) = - f x y -;; - -let rec char_list_of_string s = - let l = String.length s in - let rec aux buffer s = - function - | 0 -> buffer - | m -> aux (s.[m - 1]::buffer) s (m - 1) - in - aux [] s l -;; - -let string_of_char_list s = - let rec aux buffer = - function - | [] -> buffer - | x::xs -> aux (String.make 1 x ^ buffer) xs - in - aux "" s -;; - -(* ---------------------------------------------------------------------------- - * Haskell name management: prettyfying valid and idiomatic Haskell identifiers - * and type variable names. - * ---------------------------------------------------------------------------- - *) - -let remove_underscores_and_mark l = - let rec aux char_list_buffer positions_buffer position = - function - | [] -> (string_of_char_list char_list_buffer, positions_buffer) - | x::xs -> - if x == '_' then - aux char_list_buffer (position::positions_buffer) position xs - else - aux (x::char_list_buffer) positions_buffer (position + 1) xs - in - if l = ['_'] then "_",[] else aux [] [] 0 l -;; - -let rec capitalize_marked_positions s = - function - | [] -> s - | x::xs -> - if x < String.length s then - let c = Char.uppercase (String.get s x) in - let _ = String.set s x c in - capitalize_marked_positions s xs - else - capitalize_marked_positions s xs -;; - -let contract_underscores_and_capitalise = - char_list_of_string |> - remove_underscores_and_mark |> - uncurry capitalize_marked_positions -;; - -let idiomatic_haskell_type_name_of_string = - contract_underscores_and_capitalise |> - String.capitalize -;; - -let idiomatic_haskell_term_name_of_string = - contract_underscores_and_capitalise |> - String.uncapitalize -;; - -let classify_reference status ref = - try - match snd (ReferenceMap.find ref (fst status#extraction_db)) with - `Type _ -> `TypeName - | `Constructor _ -> `Constructor - | `Function _ -> `FunctionName - with - Not_found -> -prerr_endline ("BUG, THIS SHOULD NEVER HAPPEN " ^ NReference.string_of_reference ref); `FunctionName -;; - -let capitalize classification name = - match classification with - | `Constructor - | `TypeName -> idiomatic_haskell_type_name_of_string name - | `TypeVariable - | `BoundVariable - | `FunctionName -> idiomatic_haskell_term_name_of_string name -;; - -let pp_ref status ref = - capitalize (classify_reference status ref) - (try fst (ReferenceMap.find ref (fst status#extraction_db)) - with Not_found -> -prerr_endline ("BUG with coercions: " ^ NReference.string_of_reference ref); -(*assert false*) - NCicPp.r2s status true ref (* BUG: this should never happen *) -) - -(* cons avoid duplicates *) -let rec (@:::) name l = - if name <> "" (* propositional things *) && name.[0] = '_' then - let name = String.sub name 1 (String.length name - 1) in - let name = if name = "" then "a" else name in - name @::: l - else if List.mem name l then (name ^ "'") @::: l - else name,l -;; - -let (@::) x l = let x,l = x @::: l in x::l;; - -let rec pretty_print_type status ctxt = - function - | Var n -> List.nth ctxt (n-1) - | Unit -> "()" - | Top -> "GHC.Prim.Any" - | TConst ref -> pp_ref status ref - | Arrow (t1,t2) -> - bracket size_of_type (pretty_print_type status ctxt) t1 ^ " -> " ^ - pretty_print_type status ("_"::ctxt) t2 - | TSkip t -> pretty_print_type status ("_"::ctxt) t - | Forall (name, kind, t) -> - (*CSC: BUG HERE: avoid clashes due to uncapitalisation*) - let name = capitalize `TypeVariable name in - let name,ctxt = name@:::ctxt in - if size_of_kind kind > 1 then - "forall (" ^ name ^ " :: " ^ pretty_print_kind kind ^ "). " ^ pretty_print_type status (name::ctxt) t - else - "forall " ^ name ^ ". " ^ pretty_print_type status (name::ctxt) t - | TAppl tl -> - String.concat " " - (List.map - (fun t -> bracket ~prec:0 size_of_type - (pretty_print_type status ctxt) t) tl) -;; - -xdo_pretty_print_type := pretty_print_type;; - - -let pretty_print_term_context status ctx1 ctx2 = - let name_context, rev_res = - List.fold_right - (fun el (ctx1,rev_res) -> - match el with - None -> ""@::ctx1,rev_res - | Some (name,`OfKind _) -> - let name = capitalize `TypeVariable name in - name@::ctx1,rev_res - | Some (name,`OfType typ) -> - let name = capitalize `TypeVariable name in - let name,ctx1 = name@:::ctx1 in - name::ctx1, - ("(" ^ name ^ " :: " ^ pretty_print_type status ctx1 typ ^ ")")::rev_res - ) ctx2 (ctx1,[]) in - name_context, String.concat " " (List.rev rev_res) - -let rec pretty_print_term status ctxt = - function - | Rel n -> List.nth ctxt (n-1) - | UnitTerm -> "()" - | Const ref -> pp_ref status ref - | Lambda (name,t) -> - let name = capitalize `BoundVariable name in - let name,ctxt = name@:::ctxt in - "\\" ^ name ^ " -> " ^ pretty_print_term status (name::ctxt) t - | Appl tl -> String.concat " " (List.map (bracket size_of_term (pretty_print_term status ctxt)) tl) - | LetIn (name,s,t) -> - let name = capitalize `BoundVariable name in - let name,ctxt = name@:::ctxt in - "let " ^ name ^ " = " ^ pretty_print_term status ctxt s ^ " in " ^ - pretty_print_term status (name::ctxt) t - | BottomElim -> - "error \"Unreachable code\"" - | UnsafeCoerce t -> - "unsafeCoerce " ^ bracket size_of_term (pretty_print_term status ctxt) t - | Match (r,matched,pl) -> - if pl = [] then - "error \"Case analysis over empty type\"" - else - "case " ^ pretty_print_term status ctxt matched ^ " of {\n" ^ - String.concat " ;\n" - (HExtlib.list_mapi - (fun (bound_names,rhs) i -> - let ref = NReference.mk_constructor (i+1) r in - let name = pp_ref status ref in - let ctxt,bound_names = - pretty_print_term_context status ctxt bound_names in - let body = - pretty_print_term status ctxt rhs - in - " " ^ name ^ " " ^ bound_names ^ " -> " ^ body - ) pl) ^ "}\n " - | Skip t -> pretty_print_term status ("[[skipped]]"@::ctxt) t - | TLambda (name,t) -> - let name = capitalize `TypeVariable name in - pretty_print_term status (name@::ctxt) t - | Inst t -> pretty_print_term status ctxt t -;; - -xdo_pretty_print_term := pretty_print_term;; - -let rec pp_obj status (_,ref,obj_kind) = - let pretty_print_context ctx = - String.concat " " (List.rev (snd - (List.fold_right - (fun (x,kind) (l,res) -> - let x,l = x @:::l in - if size_of_kind kind > 1 then - x::l,("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::res - else - x::l,x::res) - (HExtlib.filter_map (fun x -> x) ctx) ([],[])))) - in - let namectx_of_ctx ctx = - List.fold_right (@::) - (List.map (function None -> "" | Some (x,_) -> x) ctx) [] in - match obj_kind with - TypeDeclaration (ctx,_) -> - (* data?? unsure semantics: inductive type without constructor, but - not matchable apparently *) - if List.length ctx = 0 then - "data " ^ pp_ref status ref - else - "data " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx - | TypeDefinition ((ctx, _),ty) -> - let namectx = namectx_of_ctx ctx in - if List.length ctx = 0 then - "type " ^ pp_ref status ref ^ " = " ^ pretty_print_type status namectx ty - else - "type " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx ^ " = " ^ pretty_print_type status namectx ty - | TermDeclaration (ctx,ty) -> - let name = pp_ref status ref in - name ^ " :: " ^ pretty_print_type status [] (glue_ctx_typ ctx ty) ^ "\n" ^ - name ^ " = error \"The declaration `" ^ name ^ "' has yet to be defined.\"" - | TermDefinition ((ctx,ty),bo) -> - let name = pp_ref status ref in - let namectx = namectx_of_ctx ctx in - (*CSC: BUG here *) - name ^ " :: " ^ pretty_print_type status namectx (glue_ctx_typ ctx ty) ^ "\n" ^ - name ^ " = " ^ pretty_print_term status namectx bo - | LetRec l -> - String.concat "\n" (List.map (pp_obj status) l) - | Algebraic il -> - String.concat "\n" - (List.map - (fun _,ref,left,right,cl -> - "data " ^ pp_ref status ref ^ " " ^ - pretty_print_context (right@left) ^ " where\n " ^ - String.concat "\n " (List.map - (fun ref,tys -> - let namectx = namectx_of_ctx left in - pp_ref status ref ^ " :: " ^ - pretty_print_type status namectx tys - ) cl) (*^ "\n deriving (Prelude.Show)"*) - ) il) - (* inductive and records missing *) - -let rec infos_of (info,_,obj_kind) = - info @ - match obj_kind with - LetRec l -> List.concat (List.map (fun (infos,_,_) -> infos) l) - | Algebraic l -> List.concat (List.map (fun (infos,_,_,_,_) -> infos) l) - | _ -> [] - -let haskell_of_obj status (uri,_,_,_,_ as obj) = - let status, obj = object_of status obj in - status, - match obj with - Erased -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to term being propositionally irrelevant.\n",[] - | OutsideTheory -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to image of term under extraction residing outside Fω.\n",[] - | Failure msg -> "-- [?] " ^ NUri.name_of_uri uri ^ " FAILURE: " ^ msg ^ "\n",[] - | Success o -> pp_obj status o ^ "\n", infos_of o - -let refresh_uri_in_typ ~refresh_uri_in_reference = - let rec refresh_uri_in_typ = - function - | Var _ - | Unit - | Top as t -> t - | TConst r -> TConst (refresh_uri_in_reference r) - | Arrow (t1,t2) -> Arrow (refresh_uri_in_typ t1, refresh_uri_in_typ t2) - | TSkip t -> TSkip (refresh_uri_in_typ t) - | Forall (n,k,t) -> Forall (n,k,refresh_uri_in_typ t) - | TAppl tl -> TAppl (List.map refresh_uri_in_typ tl) - in - refresh_uri_in_typ - -let refresh_uri_in_info ~refresh_uri_in_reference infos = - List.map - (function (ref,el) -> - match el with - name,`Constructor typ -> - let typ = refresh_uri_in_typ ~refresh_uri_in_reference typ in - refresh_uri_in_reference ref, (name,`Constructor typ) - | name,`Function typ -> - let typ = refresh_uri_in_typ ~refresh_uri_in_reference typ in - refresh_uri_in_reference ref, (name,`Function typ) - | name,`Type (ctx,typ) -> - let typ = - match typ with - None -> None - | Some t -> Some (refresh_uri_in_typ ~refresh_uri_in_reference t) - in - refresh_uri_in_reference ref, (name,`Type (ctx,typ))) - infos diff --git a/matita/components/ng_kernel/nCicExtraction.mli b/matita/components/ng_kernel/nCicExtraction.mli deleted file mode 100644 index d5cb66360..000000000 --- a/matita/components/ng_kernel/nCicExtraction.mli +++ /dev/null @@ -1,40 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -(* $Id: nCicEnvironment.mli 11172 2011-01-11 21:06:37Z sacerdot $ *) - -type info -type db - -class type g_status = - object - method extraction_db: db - end - -class virtual status : - object ('self) - inherit g_status - inherit NCic.status - method set_extraction_db: db -> 'self - method set_extraction_status: #g_status -> 'self - end - -val empty_info: info - -val refresh_uri_in_info: - refresh_uri_in_reference:(NReference.reference -> NReference.reference) -> - info -> info - -val register_infos: db -> info -> db - -(* Haskell *) -val haskell_of_obj: (#status as 'status) -> NCic.obj -> - 'status * (string * info) diff --git a/matita/components/ng_library/nCicLibrary.mli b/matita/components/ng_library/nCicLibrary.mli index b3275b828..451beaa70 100644 --- a/matita/components/ng_library/nCicLibrary.mli +++ b/matita/components/ng_library/nCicLibrary.mli @@ -21,7 +21,7 @@ class virtual status : inherit NCic.status method timestamp: timestamp method set_timestamp: timestamp -> 'self - (*CSC: bug here, we are not copying the NCicExtraction part of the status *) + (*CSC: bug here, we are not copying the NCicExtraction and OCamlExtraction part of the status *) end (* it also checks it and add it to the environment *) diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml index 144250fb9..a8e47b562 100644 --- a/matita/matita/matitaEngine.ml +++ b/matita/matita/matitaEngine.ml @@ -112,32 +112,19 @@ let pp_times ss fname rc big_bang big_bang_u big_bang_s = HLog.message ("Compilation of "^Filename.basename fname^": "^rc) ;; -let activate_extraction baseuri fname = - () - (* MATITA 1.0 - if Helm_registry.get_bool "matita.extract" then - let mangled_baseuri = - let baseuri = String.sub baseuri 5 (String.length baseuri - 5) in - let baseuri = Pcre.replace ~pat:"/" ~templ:"_" baseuri in - String.uncapitalize baseuri in - let f = - open_out - (Filename.dirname fname ^ "/" ^ mangled_baseuri ^ ".ml") in - LibrarySync.add_object_declaration_hook - (fun ~add_obj ~add_coercion _ obj -> - output_string f (CicExportation.ppobj baseuri obj); - flush f; []); - *) -;; - - let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) = let baseuri = status#baseuri in let new_aliases,new_status = GrafiteDisambiguate.eval_with_new_aliases status (fun status -> + let time0 = Unix.gettimeofday () in + let status = GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status - (text,prefix_len,ast)) in + (text,prefix_len,ast) in + let time1 = Unix.gettimeofday () in + HLog.debug ("... grafite_engine done in " ^ string_of_float (time1 -. time0) ^ "s"); + status + ) in let _,intermediate_states = List.fold_left (fun (status,acc) (k,value) -> @@ -252,9 +239,14 @@ and compile ~compiling ~asserted ~include_paths fname = let root,baseuri,fname,_tgt = Librarian.baseuri_of_script ~include_paths fname in if Http_getter_storage.is_read_only baseuri then assert false; - activate_extraction baseuri fname ; (* MATITA 1.0: debbo fare time_travel sulla ng_library? *) let status = new status baseuri in + let ocamldirname = Filename.dirname fname in + let ocamlfname = Filename.chop_extension (Filename.basename fname) in + let status,ocamlfname = + Common.modname_of_filename status false ocamlfname in + let ocamlfname = ocamldirname ^ "/" ^ ocamlfname ^ ".ml" in + let status = OcamlExtractionTable.open_file status ~baseuri ocamlfname in let big_bang = Unix.gettimeofday () in let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} = Unix.times () @@ -296,6 +288,7 @@ and compile ~compiling ~asserted ~include_paths fname = in let asserted, status = eval_from_stream ~compiling ~asserted ~include_paths status buf print_cb in + let status = OcamlExtractionTable.close_file status in let elapsed = Unix.time () -. time in (if Helm_registry.get_bool "matita.moo" then begin GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) -- 2.39.2