From cf3635c0830661f59d16339cd7fc9c3b948fcbc8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 7 Dec 2005 15:42:42 +0000 Subject: [PATCH] Big commit to let Ferruccio try the merge_coercion patch. 1) allowed :> syntax in record to specify that a field is a coercion (and it will be used (if needed) in defining the following projections) 2) minor cleanup in CicUtil.is_metaclosed 3) added library_objects.reset_defaults() (used in MatitaSync.init()) 4) added MatitaSync.init() that is the only way to obtain an initial matita status 5) CoercDb is only accessed by CoercGraph 6) insert_coercion flag added to the refiner (and removed the use_coercion flag from CoercDb). Coercions are always available, the refiner will eventually insert them 7) CicRefiner now packs coercions with the avoid_double_coercion function 8) GrafiteAstPp is now "more" in sync and dump_moo seems to work again 9) LibrarySync has a merge_coercions function that calls on `Generated && not(is_coercion) objects. I hope it is enough (calling it on every objects shlows down a bit 10)MatitaScript now calls MatitaSync.init() on reset TODO: - remove CoercGraph.remove_coercion from add_single_obj - find a place for CoercGraph.add_coercion used in generate_projections --- helm/ocaml/acic_content/cicNotationPp.ml | 4 +- helm/ocaml/acic_content/cicNotationPt.ml | 2 +- helm/ocaml/acic_content/cicNotationUtil.ml | 3 +- helm/ocaml/cic/.depend | 4 +- helm/ocaml/cic/cic.ml | 5 +- helm/ocaml/cic/cicParser.ml | 8 +- helm/ocaml/cic/cicUtil.ml | 21 +-- helm/ocaml/cic/libraryObjects.ml | 17 ++ helm/ocaml/cic/libraryObjects.mli | 2 + helm/ocaml/cic_acic/cic2Xml.ml | 6 +- helm/ocaml/cic_disambiguation/disambiguate.ml | 8 +- helm/ocaml/cic_unification/cicRefine.ml | 147 ++++++++++++------ helm/ocaml/cic_unification/cicRefine.mli | 3 + helm/ocaml/content_pres/.depend | 16 +- helm/ocaml/grafite/grafiteAstPp.ml | 70 ++++++--- helm/ocaml/grafite2/matitaSync.ml | 39 ++++- helm/ocaml/grafite2/matitaSync.mli | 5 + helm/ocaml/grafite_parser/.depend | 4 +- helm/ocaml/grafite_parser/grafiteParser.ml | 4 +- .../grafite_parser/matitaDisambiguator.ml | 10 +- helm/ocaml/library/.depend | 8 +- helm/ocaml/library/Makefile | 2 +- helm/ocaml/library/cicRecord.ml | 23 ++- helm/ocaml/library/coercDb.ml | 14 +- helm/ocaml/library/coercDb.mli | 12 +- helm/ocaml/library/coercGraph.ml | 135 ++++++++-------- helm/ocaml/library/coercGraph.mli | 13 +- helm/ocaml/library/librarySync.ml | 108 ++++++++++++- helm/ocaml/library/librarySync.mli | 2 + helm/ocaml/tactics/.depend | 8 +- helm/ocaml/tactics/doc/body.tex | 110 ++++++------- helm/ocaml/tactics/doc/main.tex | 1 + 32 files changed, 542 insertions(+), 272 deletions(-) diff --git a/helm/ocaml/acic_content/cicNotationPp.ml b/helm/ocaml/acic_content/cicNotationPp.ml index bf0f9ed4c..0813c732a 100644 --- a/helm/ocaml/acic_content/cicNotationPp.ml +++ b/helm/ocaml/acic_content/cicNotationPp.ml @@ -255,7 +255,9 @@ let pp_flavour = function let pp_fields fields = (if fields <> [] then "\n" else "") ^ String.concat ";\n" - (List.map (fun (name,ty) -> " " ^ name ^ ": " ^ pp_term ty) fields) + (List.map + (fun (name,ty,coercion) -> + " " ^ name ^ if coercion then ":>" else ": " ^ pp_term ty) fields) let pp_obj = function | Ast.Inductive (params, types) -> diff --git a/helm/ocaml/acic_content/cicNotationPt.ml b/helm/ocaml/acic_content/cicNotationPt.ml index e3d5fc544..d2a32c779 100644 --- a/helm/ocaml/acic_content/cicNotationPt.ml +++ b/helm/ocaml/acic_content/cicNotationPt.ml @@ -171,7 +171,7 @@ type obj = * - body is present when its given along with the command, otherwise it * will be given in proof editing mode using the tactical language *) - | Record of (string * term) list * string * term * (string * term) list + | Record of (string * term) list * string * term * (string * term * bool) list (** left parameters, name, type, fields *) (** {2 Standard precedences} *) diff --git a/helm/ocaml/acic_content/cicNotationUtil.ml b/helm/ocaml/acic_content/cicNotationUtil.ml index 0aa6b48b3..285047de8 100644 --- a/helm/ocaml/acic_content/cicNotationUtil.ml +++ b/helm/ocaml/acic_content/cicNotationUtil.ml @@ -364,6 +364,7 @@ let freshen_obj obj = let index = ref 0 in let freshen_term = freshen_term ~index in let freshen_name_ty = List.map (fun (n, t) -> (n, freshen_term t)) in + let freshen_name_ty_b = List.map (fun (n, t, b) -> (n, freshen_term t, b)) in match obj with | CicNotationPt.Inductive (params, indtypes) -> let indtypes = @@ -379,7 +380,7 @@ let freshen_obj obj = CicNotationPt.Theorem (flav, n, freshen_term t, ty_opt) | CicNotationPt.Record (params, n, ty, fields) -> CicNotationPt.Record (freshen_name_ty params, n, freshen_term ty, - freshen_name_ty fields) + freshen_name_ty_b fields) let freshen_term = freshen_term ?index:None diff --git a/helm/ocaml/cic/.depend b/helm/ocaml/cic/.depend index 45305130d..2db97d7bb 100644 --- a/helm/ocaml/cic/.depend +++ b/helm/ocaml/cic/.depend @@ -13,8 +13,8 @@ deannotate.cmo: cic.cmo deannotate.cmi deannotate.cmx: cic.cmx deannotate.cmi cicParser.cmo: deannotate.cmi cicUniv.cmi cic.cmo cicParser.cmi cicParser.cmx: deannotate.cmx cicUniv.cmx cic.cmx cicParser.cmi -cicUtil.cmo: cic.cmo cicUtil.cmi -cicUtil.cmx: cic.cmx cicUtil.cmi +cicUtil.cmo: cicUniv.cmi cic.cmo cicUtil.cmi +cicUtil.cmx: cicUniv.cmx cic.cmx cicUtil.cmi helmLibraryObjects.cmo: cic.cmo helmLibraryObjects.cmi helmLibraryObjects.cmx: cic.cmx helmLibraryObjects.cmi libraryObjects.cmo: helmLibraryObjects.cmi libraryObjects.cmi diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml index 624a30216..4b4e0fed9 100644 --- a/helm/ocaml/cic/cic.ml +++ b/helm/ocaml/cic/cic.ml @@ -66,8 +66,9 @@ type object_class = [ `Coercion | `Elim of sort (** elimination principle; if sort is Type, the universe is * not relevant *) - | `Record of string list (** inductive type that encodes a record; - the arguments are the record fields *) + | `Record of (string * bool) list (** + inductive type that encodes a record; the arguments are + the record fields names and if they are coercions *) | `Projection (** record projection *) ] diff --git a/helm/ocaml/cic/cicParser.ml b/helm/ocaml/cic/cicParser.ml index d81521f99..68f1257d1 100644 --- a/helm/ocaml/cic/cicParser.ml +++ b/helm/ocaml/cic/cicParser.ml @@ -686,7 +686,13 @@ let end_element ctxt tag = let fields = List.map (function - | Obj_field name -> name + | Obj_field name -> + (match Str.split (Str.regexp " ") name with + | [name] -> name, false + | [name;"coercion"] -> name,true + | _ -> + parse_error + "wrong \"field\"'s name attribute") | _ -> parse_error "unexpected extra content for \"record\" object class") diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml index bb356655a..1af68ce39 100644 --- a/helm/ocaml/cic/cicUtil.ml +++ b/helm/ocaml/cic/cicUtil.ml @@ -115,24 +115,25 @@ let rec is_meta_closed = | Cic.Lambda (_,so,dest) -> is_meta_closed so && is_meta_closed dest | Cic.LetIn (_,so,dest) -> is_meta_closed so && is_meta_closed dest | Cic.Appl l -> - List.fold_right (fun x i -> i && is_meta_closed x) l true + not (List.exists (fun x -> not (is_meta_closed x)) l) | Cic.Var (_,exp_named_subst) | Cic.Const (_,exp_named_subst) | Cic.MutInd (_,_,exp_named_subst) | Cic.MutConstruct (_,_,_,exp_named_subst) -> - List.fold_right (fun (_,x) i -> i && is_meta_closed x) - exp_named_subst true + not (List.exists (fun (_,x) -> not (is_meta_closed x)) exp_named_subst) | Cic.MutCase (_,_,out,te,pl) -> is_meta_closed out && is_meta_closed te && - List.fold_right (fun x i -> i && is_meta_closed x) pl true + not (List.exists (fun x -> not (is_meta_closed x)) pl) | Cic.Fix (_,fl) -> - List.fold_right - (fun (_,_,ty,bo) i -> i && is_meta_closed ty && is_meta_closed bo - ) fl true + not (List.exists + (fun (_,_,ty,bo) -> + not (is_meta_closed ty) || not (is_meta_closed bo)) + fl) | Cic.CoFix (_,fl) -> - List.fold_right - (fun (_,ty,bo) i -> i && is_meta_closed ty && is_meta_closed bo - ) fl true + not (List.exists + (fun (_,ty,bo) -> + not (is_meta_closed ty) || not (is_meta_closed bo)) + fl) ;; let xpointer_RE = Str.regexp "\\([^#]+\\)#xpointer(\\(.*\\))" diff --git a/helm/ocaml/cic/libraryObjects.ml b/helm/ocaml/cic/libraryObjects.ml index 967318721..353710708 100644 --- a/helm/ocaml/cic/libraryObjects.ml +++ b/helm/ocaml/cic/libraryObjects.ml @@ -25,6 +25,17 @@ (**** TABLES ****) +let default_eq_URIs = + [HelmLibraryObjects.Logic.eq_URI, + HelmLibraryObjects.Logic.sym_eq_URI, + HelmLibraryObjects.Logic.trans_eq_URI, + HelmLibraryObjects.Logic.eq_ind_URI, + HelmLibraryObjects.Logic.eq_ind_r_URI];; + +let default_true_URIs = [HelmLibraryObjects.Logic.true_URI] +let default_false_URIs = [HelmLibraryObjects.Logic.false_URI] +let default_absurd_URIs = [HelmLibraryObjects.Logic.absurd_URI] + (* eq, sym_eq, trans_eq, eq_ind, eq_ind_R *) let eq_URIs_ref = ref [HelmLibraryObjects.Logic.eq_URI, @@ -65,6 +76,12 @@ let set_default what l = absurd_URIs_ref := insert_unique absurd_URI (fun x -> x) !absurd_URIs_ref | _,_ -> raise NotRecognized +let reset_defaults () = + eq_URIs_ref := default_eq_URIs; + true_URIs_ref := default_true_URIs; + false_URIs_ref := default_false_URIs; + absurd_URIs_ref := default_absurd_URIs + (**** LOOKUP FUNCTIONS ****) let eq_URI () = let eq,_,_,_,_ = List.hd !eq_URIs_ref in eq diff --git a/helm/ocaml/cic/libraryObjects.mli b/helm/ocaml/cic/libraryObjects.mli index 3ca7e7292..f87065980 100644 --- a/helm/ocaml/cic/libraryObjects.mli +++ b/helm/ocaml/cic/libraryObjects.mli @@ -24,6 +24,7 @@ *) val set_default : string -> UriManager.uri list -> unit +val reset_defaults : unit -> unit val eq_URI : unit -> UriManager.uri @@ -40,3 +41,4 @@ val sym_eq_URI : eq:UriManager.uri -> UriManager.uri val false_URI : unit -> UriManager.uri val true_URI : unit -> UriManager.uri val absurd_URI : unit -> UriManager.uri + diff --git a/helm/ocaml/cic_acic/cic2Xml.ml b/helm/ocaml/cic_acic/cic2Xml.ml index 5bd9fd1c9..4d5cb00de 100644 --- a/helm/ocaml/cic_acic/cic2Xml.ml +++ b/helm/ocaml/cic_acic/cic2Xml.ml @@ -277,8 +277,10 @@ let xml_of_attrs attributes = | `Record field_names -> Xml.xml_nempty "class" [None,"value","record"] (List.fold_right - (fun name res -> - [< Xml.xml_empty "field" [None,"name",name]; res >] + (fun (name,coercion) res -> + [< Xml.xml_empty "field" + [None,"name",if coercion then name ^ " coercion" else name]; + res >] ) field_names [<>]) | `Projection -> Xml.xml_empty "class" [None,"value","projection"] in diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index bee671ee8..f1d53de52 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -489,7 +489,7 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl = let fields' = snd ( List.fold_left - (fun (context,res) (name,ty) -> + (fun (context,res) (name,ty,_coercion) -> let context' = Cic.Name name :: context in context',(name,interpretate_term context env None false ty)::res ) (context,[]) fields) in @@ -506,7 +506,7 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl = concl fields' in let con' = add_params con in let tyl = [name,true,ty',["mk_" ^ name,con']] in - let field_names = List.map fst fields in + let field_names = List.map (fun (x,_,y) -> x,y) fields in Cic.InductiveDefinition (tyl,[],List.length params,[`Class (`Record field_names)]) | CicNotationPt.Theorem (flavour, name, ty, bo) -> @@ -688,12 +688,12 @@ let domain_of_obj ~context ast = | CicNotationPt.Record (params,_,ty,fields) -> let dom = List.flatten - (List.rev_map (fun (_,ty) -> domain_rev_of_term [] ty) fields) in + (List.rev_map (fun (_,ty,_) -> domain_rev_of_term [] ty) fields) in let dom = List.filter (fun name-> not ( List.exists (fun (name',_) -> name = Id name') params - || List.exists (fun (name',_) -> name = Id name') fields) + || List.exists (fun (name',_,_) -> name = Id name') fields) ) dom in List.fold_left diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 9c78c1aa7..e1c1e91ce 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -29,6 +29,8 @@ exception RefineFailure of string Lazy.t;; exception Uncertain of string Lazy.t;; exception AssertFailure of string Lazy.t;; +let insert_coercions = ref true + let debug_print = fun _ -> () let profiler = HExtlib.profile "CicRefine.fo_unif" @@ -90,6 +92,7 @@ let exp_impl metasenv subst context = | _ -> assert false ;; + let rec type_of_constant uri ugraph = let module C = Cic in let module R = CicReduction in @@ -305,28 +308,46 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t let coerce_to_sort in_source tgt_sort t type_to_coerce subst context metasenv uragph = - let coercion_src = carr type_to_coerce subst context in - match coercion_src with - | Cic.Sort _ -> - t,type_to_coerce,subst,metasenv,ugraph - | Cic.Meta _ as meta -> - t, meta, subst, metasenv, ugraph - | Cic.Cast _ as cast -> - t, cast, subst, metasenv, ugraph - | term -> - let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in - let search = CoercGraph.look_for_coercion in - let boh = search coercion_src coercion_tgt in - (match boh with - | CoercGraph.NoCoercion - | CoercGraph.NotHandled _ -> - enrich localization_tbl t - (RefineFailure (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst t context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort"))) - | CoercGraph.NotMetaClosed -> - enrich localization_tbl t - (Uncertain (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst t context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort"))) - | CoercGraph.SomeCoercion c -> - Cic.Appl [c;t],Cic.Sort tgt_sort,subst, metasenv, ugraph) + if not !insert_coercions then + t,type_to_coerce,subst,metasenv,ugraph + else + let coercion_src = carr type_to_coerce subst context in + match coercion_src with + | Cic.Sort _ -> + t,type_to_coerce,subst,metasenv,ugraph + | Cic.Meta _ as meta -> + t, meta, subst, metasenv, ugraph + | Cic.Cast _ as cast -> + t, cast, subst, metasenv, ugraph + | term -> + let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in + let search = CoercGraph.look_for_coercion in + let boh = search coercion_src coercion_tgt in + (match boh with + | CoercGraph.NoCoercion + | CoercGraph.NotHandled _ -> + enrich localization_tbl t + (RefineFailure + (lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst t context ^ + " is not a type since it has type " ^ + CicMetaSubst.ppterm_in_context + subst coercion_src context ^ " that is not a sort"))) + | CoercGraph.NotMetaClosed -> + enrich localization_tbl t + (Uncertain + (lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst t context ^ + " is not a type since it has type " ^ + CicMetaSubst.ppterm_in_context + subst coercion_src context ^ " that is not a sort"))) + | CoercGraph.SomeCoercion c -> + let newt, tty, subst, metasenv, ugraph = + avoid_double_coercion + subst metasenv ugraph + (Cic.Appl[c;t]) coercion_tgt + in + newt, tty, subst, metasenv, ugraph) in let s',sort1,subst',metasenv',ugraph1 = type_of_aux subst metasenv context s ugraph @@ -353,24 +374,41 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t let s',sort1,subst',metasenv',ugraph1 = type_of_aux subst metasenv context s ugraph in - let s',sort1 = - match CicReduction.whd ~subst:subst' context sort1 with - C.Meta _ - | C.Sort _ -> s',sort1 - | coercion_src -> - let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh ())) in - let search = CoercGraph.look_for_coercion in - let boh = search coercion_src coercion_tgt in - match boh with - | CoercGraph.SomeCoercion c -> - Cic.Appl [c;s'], coercion_tgt - | CoercGraph.NoCoercion - | CoercGraph.NotHandled _ -> - enrich localization_tbl s' - (RefineFailure (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst s' context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort"))) - | CoercGraph.NotMetaClosed -> - enrich localization_tbl s' - (Uncertain (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst s' context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort"))) + let s',sort1,subst',metasenv',ugraph1 = + if not !insert_coercions then + s',sort1, subst', metasenv', ugraph1 + else + match CicReduction.whd ~subst:subst' context sort1 with + | C.Meta _ | C.Sort _ -> s',sort1, subst', metasenv', ugraph1 + | coercion_src -> + let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in + let search = CoercGraph.look_for_coercion in + let boh = search coercion_src coercion_tgt in + match boh with + | CoercGraph.SomeCoercion c -> + let newt, tty, subst', metasenv', ugraph1 = + avoid_double_coercion + subst' metasenv' ugraph1 + (Cic.Appl[c;s']) coercion_tgt + in + newt, tty, subst', metasenv', ugraph1 + | CoercGraph.NoCoercion + | CoercGraph.NotHandled _ -> + enrich localization_tbl s' + (RefineFailure + (lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst s' context ^ + " is not a type since it has type " ^ + CicMetaSubst.ppterm_in_context + subst coercion_src context ^ " that is not a sort"))) + | CoercGraph.NotMetaClosed -> + enrich localization_tbl s' + (Uncertain + (lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst s' context ^ + " is not a type since it has type " ^ + CicMetaSubst.ppterm_in_context + subst coercion_src context ^ " that is not a sort"))) in let context_for_t = ((Some (n,(C.Decl s')))::context) in let t',type2,subst'',metasenv'',ugraph2 = @@ -412,7 +450,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t eat_prods true subst'' metasenv'' context hetype tlbody_and_type ugraph2 in - C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3 + avoid_double_coercion + subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty | C.Appl _ -> assert false | C.Const (uri,exp_named_subst) -> let exp_named_subst',subst',metasenv',ugraph1 = @@ -810,6 +849,19 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t relocalize localization_tbl t t'; res + and avoid_double_coercion subst metasenv ugraph t ty = + match t with + | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) as t when + CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 -> + let source_carr = CoercGraph.source_of c2 in + let tgt_carr = CicMetaSubst.apply_subst subst ty in + (match CoercGraph.look_for_coercion source_carr tgt_carr + with + | CoercGraph.SomeCoercion c -> + Cic.Appl [ c ; head ], ty, subst,metasenv,ugraph + | _ -> assert false) (* the composite coercion must exist *) + | _ -> t, ty, subst, metasenv, ugraph + (* check_metasenv_consistency checks that the "canonical" context of a metavariable is consitent - up to relocation via the relocation list l - with the actual context *) @@ -1025,15 +1077,15 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t fo_unif_subst subst context metasenv hety s ugraph in hete,subst,metasenv,ugraph1 - with exn when allow_coercions -> + with exn when allow_coercions && !insert_coercions -> (* we search a coercion from hety to s *) - let coer = + let coer, tgt_carr = let carr t subst context = CicMetaSubst.apply_subst subst t in let c_hety = carr hety subst context in let c_s = carr s subst context in - CoercGraph.look_for_coercion c_hety c_s + CoercGraph.look_for_coercion c_hety c_s, c_s in match coer with | CoercGraph.NoCoercion @@ -1058,7 +1110,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t CicMetaSubst.ppterm_in_context subst s context (* "\nReason: " ^ Lazy.force e*)))) | CoercGraph.SomeCoercion c -> - (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph + let newt, _, subst, metasenv, ugraph = + avoid_double_coercion + subst metasenv ugraph + (Cic.Appl[c;hete]) tgt_carr + in + newt, subst, metasenv, ugraph in let coerced_args,metasenv',subst',t',ugraph2 = eat_prods metasenv subst context diff --git a/helm/ocaml/cic_unification/cicRefine.mli b/helm/ocaml/cic_unification/cicRefine.mli index 97417f7f6..224a7586c 100644 --- a/helm/ocaml/cic_unification/cicRefine.mli +++ b/helm/ocaml/cic_unification/cicRefine.mli @@ -43,3 +43,6 @@ val typecheck : localization_tbl:Token.flocation Cic.CicHash.t -> Cic.metasenv -> UriManager.uri option -> Cic.obj -> Cic.obj * Cic.metasenv * CicUniv.universe_graph + +val insert_coercions: bool ref (* initially true *) + diff --git a/helm/ocaml/content_pres/.depend b/helm/ocaml/content_pres/.depend index 781c9e45b..60e25ecd8 100644 --- a/helm/ocaml/content_pres/.depend +++ b/helm/ocaml/content_pres/.depend @@ -26,11 +26,11 @@ boxPp.cmo: renderingAttrs.cmi mpresentation.cmi cicNotationPres.cmi box.cmi \ boxPp.cmi boxPp.cmx: renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \ boxPp.cmi -content2pres.cmo: renderingAttrs.cmi mpresentation.cmi cicNotationPres.cmi \ - box.cmi content2pres.cmi -content2pres.cmx: renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx \ - box.cmx content2pres.cmi -sequent2pres.cmo: mpresentation.cmi cicNotationPres.cmi box.cmi \ - sequent2pres.cmi -sequent2pres.cmx: mpresentation.cmx cicNotationPres.cmx box.cmx \ - sequent2pres.cmi +content2pres.cmo: termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \ + cicNotationPres.cmi box.cmi content2pres.cmi +content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \ + cicNotationPres.cmx box.cmx content2pres.cmi +sequent2pres.cmo: termContentPres.cmi mpresentation.cmi cicNotationPres.cmi \ + box.cmi sequent2pres.cmi +sequent2pres.cmx: termContentPres.cmx mpresentation.cmx cicNotationPres.cmx \ + box.cmx sequent2pres.cmi diff --git a/helm/ocaml/grafite/grafiteAstPp.ml b/helm/ocaml/grafite/grafiteAstPp.ml index ce4a585b3..dac1d6e05 100644 --- a/helm/ocaml/grafite/grafiteAstPp.ml +++ b/helm/ocaml/grafite/grafiteAstPp.ml @@ -206,30 +206,47 @@ let pp_dir_opt = function | Some `LeftToRight -> "> " | Some `RightToLeft -> "< " +let pp_interpretation dsc symbol arg_patterns cic_appl_pattern = + sprintf "interpretation \"%s\" '%s %s = %s" + dsc symbol + (String.concat " " (List.map pp_argument_pattern arg_patterns)) + (CicNotationPp.pp_cic_appl_pattern cic_appl_pattern) + +let pp_default what uris = + sprintf "default \"%s\" %s" what + (String.concat " " (List.map UriManager.string_of_uri uris)) + +let pp_notation dir_opt l1_pattern assoc prec l2_pattern = + sprintf "notation %s\"%s\" %s %s for %s" + (pp_dir_opt dir_opt) + (pp_l1_pattern l1_pattern) + (pp_associativity assoc) + (pp_precedence prec) + (pp_l2_pattern l2_pattern) + +let pp_coercion_ast term do_composites = + sprintf "coercion %s (* %s *)" (pp_term_ast term) + (if do_composites then "compounds" else "no compounds") + +let pp_coercion_cic term do_composites = + sprintf "coercion %s (* %s *)" (pp_term_cic term) + (if do_composites then "compounds" else "no compounds") + let pp_command = function | Include (_,path) -> "include " ^ path | Qed _ -> "qed" | Drop _ -> "drop" | Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value - | Coercion (_,term, _do_composites) -> - sprintf "coercion %s" (pp_term_ast term) + | Coercion (_,term, do_composites) -> + pp_coercion_ast term do_composites | Alias (_,s) -> pp_alias s | Obj (_,obj) -> CicNotationPp.pp_obj obj | Default (_,what,uris) -> - sprintf "default \"%s\" %s" what - (String.concat " " (List.map UriManager.string_of_uri uris)) + pp_default what uris | Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) -> - sprintf "interpretation \"%s\" '%s %s = %s" - dsc symbol - (String.concat " " (List.map pp_argument_pattern arg_patterns)) - (CicNotationPp.pp_cic_appl_pattern cic_appl_pattern) + pp_interpretation dsc symbol arg_patterns cic_appl_pattern | Notation (_, dir_opt, l1_pattern, assoc, prec, l2_pattern) -> - sprintf "notation %s\"%s\" %s %s for %s" - (pp_dir_opt dir_opt) - (pp_l1_pattern l1_pattern) - (pp_associativity assoc) - (pp_precedence prec) - (pp_l2_pattern l2_pattern) + pp_notation dir_opt l1_pattern assoc prec l2_pattern | Render _ | Dump _ -> assert false (* ZACK: debugging *) @@ -275,20 +292,25 @@ let pp_statement = function | Executable (_, ex) -> pp_executable ex | Comment (_, c) -> pp_comment c + + let pp_cic_command = function | Include (_,path) -> "include " ^ path | Qed _ -> "qed" | Drop _ -> "drop" - | Coercion (_,term,_add_composites) -> - sprintf "coercion %s" (CicPp.ppterm term) - | Set _ - | Alias _ - | Default _ - | Render _ - | Dump _ - | Interpretation _ - | Notation _ - | Obj _ -> assert false (* not implemented *) + | Coercion (_,term, do_composites) -> + pp_coercion_cic term do_composites + | Obj (_,obj) -> CicPp.ppobj obj + | Set _-> assert false (* not implemented *) + | Alias (_, alias) -> pp_alias alias + | Default (_,what,uris) -> + pp_default what uris + | Render _ -> assert false (* not implemented *) + | Dump _ -> assert false (* not implemented *) + | Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) -> + pp_interpretation dsc symbol arg_patterns cic_appl_pattern + | Notation (_, dir_opt, l1_pattern, assoc, prec, l2_pattern) -> + pp_notation dir_opt l1_pattern assoc prec l2_pattern let pp_dependency = function | IncludeDep str -> "include \"" ^ str ^ "\"" diff --git a/helm/ocaml/grafite2/matitaSync.ml b/helm/ocaml/grafite2/matitaSync.ml index 2424d178f..0f019a692 100644 --- a/helm/ocaml/grafite2/matitaSync.ml +++ b/helm/ocaml/grafite2/matitaSync.ml @@ -127,14 +127,24 @@ let add_obj = let add_coercion status ~add_composites uri = let basedir = Helm_registry.get "matita.basedir" in - let lemmas = CoercGraph.add_coercion ~basedir ~add_composites uri in - let status = {status with coercions = uri :: status.coercions} in + let compounds = CoercGraph.add_coercion uri in + let status = + if add_composites then + (List.iter (fun (u,_) -> + prerr_endline (UriManager.string_of_uri u)) compounds; + List.fold_left (fun s (uri,o) -> add_obj uri o s) status compounds ) + else + status + in + let status = + {status with coercions = uri :: List.map fst compounds @ status.coercions} + in let statement_of name = - GrafiteAst.Coercion - (DisambiguateTypes.dummy_floc, CicUtil.term_of_uri uri, false) in + GrafiteAst.Coercion + (DisambiguateTypes.dummy_floc, CicUtil.term_of_uri uri, false) in let moo_content = [statement_of (UriManager.name_of_uri uri)] in let status = GrafiteTypes.add_moo_content moo_content status in - List.fold_left add_alias_for_constant status lemmas + List.fold_left add_alias_for_constant status (List.map fst compounds) module OrderedUri = struct @@ -175,7 +185,24 @@ let time_travel ~present ~past = in let debug_list = ref [] in List.iter - (fun uri -> CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri)) + (fun uri -> CoercGraph.remove_coercion uri) coercions_to_remove; List.iter LibrarySync.remove_obj objs_to_remove; List.iter CicNotation.remove_notation notation_to_remove + +let init () = + CoercGraph.remove_all (); + LibraryObjects.reset_defaults (); + { + aliases = DisambiguateTypes.Environment.empty; + multi_aliases = DisambiguateTypes.Environment.empty; + moo_content_rev = []; + metadata = []; + proof_status = No_proof; + options = no_options; + objects = []; + coercions = []; + notation_ids = []; + } + + diff --git a/helm/ocaml/grafite2/matitaSync.mli b/helm/ocaml/grafite2/matitaSync.mli index df4f111ab..6161a6a0d 100644 --- a/helm/ocaml/grafite2/matitaSync.mli +++ b/helm/ocaml/grafite2/matitaSync.mli @@ -47,3 +47,8 @@ val set_proof_aliases : GrafiteTypes.status -> (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list -> GrafiteTypes.status + + (* also resets the imperative part of the status *) +val init: unit -> GrafiteTypes.status + + diff --git a/helm/ocaml/grafite_parser/.depend b/helm/ocaml/grafite_parser/.depend index 6d2222906..0694143fc 100644 --- a/helm/ocaml/grafite_parser/.depend +++ b/helm/ocaml/grafite_parser/.depend @@ -6,5 +6,5 @@ matitaDisambiguator.cmo: matitaDisambiguator.cmi matitaDisambiguator.cmx: matitaDisambiguator.cmi grafiteDisambiguate.cmo: matitaDisambiguator.cmi grafiteDisambiguate.cmi grafiteDisambiguate.cmx: matitaDisambiguator.cmx grafiteDisambiguate.cmi -grafiteParserMisc.cmo: grafiteParserMisc.cmi -grafiteParserMisc.cmx: grafiteParserMisc.cmi +grafiteParserMisc.cmo: grafiteParser.cmi grafiteParserMisc.cmi +grafiteParserMisc.cmx: grafiteParser.cmx grafiteParserMisc.cmi diff --git a/helm/ocaml/grafite_parser/grafiteParser.ml b/helm/ocaml/grafite_parser/grafiteParser.ml index 64db52295..f76528567 100644 --- a/helm/ocaml/grafite_parser/grafiteParser.ml +++ b/helm/ocaml/grafite_parser/grafiteParser.ml @@ -304,7 +304,9 @@ EXTEND name = IDENT; params = LIST0 [ arg = arg -> arg ] ; SYMBOL ":"; typ = term; SYMBOL <:unicode>; SYMBOL "{" ; fields = LIST0 [ - name = IDENT ; SYMBOL ":" ; ty = term -> (name,ty) + name = IDENT ; + coercion = [ SYMBOL ":" -> false | SYMBOL ":"; SYMBOL ">" -> true ] ; + ty = term -> (name,ty,coercion) ] SEP SYMBOL ";"; SYMBOL "}" -> let params = List.fold_right diff --git a/helm/ocaml/grafite_parser/matitaDisambiguator.ml b/helm/ocaml/grafite_parser/matitaDisambiguator.ml index 88ef32b7a..5258a4963 100644 --- a/helm/ocaml/grafite_parser/matitaDisambiguator.ml +++ b/helm/ocaml/grafite_parser/matitaDisambiguator.ml @@ -94,8 +94,8 @@ let disambiguate_thing ~aliases ~universe (true, library, true); ] in - let try_pass (fresh_instances, (_, aliases, universe), use_coercions) = - CoercDb.use_coercions := use_coercions; + let try_pass (fresh_instances, (_, aliases, universe), insert_coercions) = + CicRefine.insert_coercions := insert_coercions; f ~fresh_instances ~aliases ~universe thing in let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) = @@ -120,13 +120,13 @@ let disambiguate_thing ~aliases ~universe aux (errors @ [newerrors]) tl) | [] -> assert false in - let saved_use_coercions = !CoercDb.use_coercions in + let saved_insert_coercions = !CicRefine.insert_coercions in try let res = aux [] passes in - CoercDb.use_coercions := saved_use_coercions; + CicRefine.insert_coercions := saved_insert_coercions; res with exn -> - CoercDb.use_coercions := saved_use_coercions; + CicRefine.insert_coercions := saved_insert_coercions; raise exn type disambiguator_thing = diff --git a/helm/ocaml/library/.depend b/helm/ocaml/library/.depend index 279a4ea65..0e1060c9e 100644 --- a/helm/ocaml/library/.depend +++ b/helm/ocaml/library/.depend @@ -8,12 +8,12 @@ libraryDb.cmo: libraryDb.cmi libraryDb.cmx: libraryDb.cmi coercDb.cmo: coercDb.cmi coercDb.cmx: coercDb.cmi -librarySync.cmo: libraryDb.cmi coercDb.cmi cicRecord.cmi cicElim.cmi \ +coercGraph.cmo: coercDb.cmi coercGraph.cmi +coercGraph.cmx: coercDb.cmx coercGraph.cmi +librarySync.cmo: libraryDb.cmi coercGraph.cmi cicRecord.cmi cicElim.cmi \ librarySync.cmi -librarySync.cmx: libraryDb.cmx coercDb.cmx cicRecord.cmx cicElim.cmx \ +librarySync.cmx: libraryDb.cmx coercGraph.cmx cicRecord.cmx cicElim.cmx \ librarySync.cmi -coercGraph.cmo: librarySync.cmi coercDb.cmi coercGraph.cmi -coercGraph.cmx: librarySync.cmx coercDb.cmx coercGraph.cmi libraryNoDb.cmo: libraryNoDb.cmi libraryNoDb.cmx: libraryNoDb.cmi libraryClean.cmo: librarySync.cmi libraryNoDb.cmi libraryMisc.cmi \ diff --git a/helm/ocaml/library/Makefile b/helm/ocaml/library/Makefile index ee07c8162..581709b2c 100644 --- a/helm/ocaml/library/Makefile +++ b/helm/ocaml/library/Makefile @@ -7,8 +7,8 @@ INTERFACE_FILES = \ libraryMisc.mli \ libraryDb.mli \ coercDb.mli \ - librarySync.mli \ coercGraph.mli \ + librarySync.mli \ libraryNoDb.mli \ libraryClean.mli \ $(NULL) diff --git a/helm/ocaml/library/cicRecord.ml b/helm/ocaml/library/cicRecord.ml index a251bad87..85c2ea036 100644 --- a/helm/ocaml/library/cicRecord.ml +++ b/helm/ocaml/library/cicRecord.ml @@ -34,7 +34,6 @@ let generate_one_proj uri params paramsno fields t i = Cic.Lambda (Cic.Name name,ty,acc)) l start in let recty = rec_ty uri paramsno in let outtype = Cic.Lambda (Cic.Name "w'", CicSubstitution.lift 1 recty, t) in - Some (mk_lambdas params (Cic.Lambda (Cic.Name "w", recty, Cic.MutCase (uri,0,outtype, Cic.Rel 1, @@ -72,19 +71,15 @@ let projections_of uri field_names = Cic.MutInd _, [] | Cic.Appl _, [] -> [] | Cic.Prod (_,s,t), name::tl -> - (match generate_one_proj uri leftparams paramsno fields s i with - Some p -> - let puri = - UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") - in - (puri,name,p) :: - aux (i - 1) - (CicSubstitution.subst - (Cic.Appl - (Cic.Const (puri,[]) :: - CicUtil.mk_rels paramsno 2 @ [Cic.Rel 1]) - ) t, tl) - | None -> assert false) + let p = generate_one_proj uri leftparams paramsno fields s i in + let puri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") in + (puri,name,p) :: + aux (i - 1) + (CicSubstitution.subst + (Cic.Appl + (Cic.Const (puri,[]) :: + CicUtil.mk_rels paramsno 2 @ [Cic.Rel 1]) + ) t, tl) | _,_ -> assert false in aux (List.length fields) (CicSubstitution.lift 2 ty,field_names) diff --git a/helm/ocaml/library/coercDb.ml b/helm/ocaml/library/coercDb.ml index 437ad65ae..bc3d2a745 100644 --- a/helm/ocaml/library/coercDb.ml +++ b/helm/ocaml/library/coercDb.ml @@ -28,7 +28,6 @@ exception EqCarrNotImplemented of string Lazy.t exception EqCarrOnNonMetaClosed let db = ref [] -let use_coercions = ref true let coerc_carr_of_term t = try @@ -69,7 +68,14 @@ let remove_coercion p = db := List.filter (fun u -> not(p u)) !db let find_coercion f = - if !use_coercions then - List.map (fun (_,_,x) -> x) (List.filter (fun (s,t,_) -> f (s,t)) !db) - else [] + List.map (fun (_,_,x) -> x) (List.filter (fun (s,t,_) -> f (s,t)) !db) + +let is_a_coercion u = + List.exists (fun (_,_,x) -> UriManager.eq x u) !db + +let get_carr uri = + try + let src, tgt, _ = List.find (fun (_,_,x) -> UriManager.eq x uri) !db in + src, tgt + with Not_found -> assert false (* uri must be a coercion *) diff --git a/helm/ocaml/library/coercDb.mli b/helm/ocaml/library/coercDb.mli index 2d7a11cae..970d2b98a 100644 --- a/helm/ocaml/library/coercDb.mli +++ b/helm/ocaml/library/coercDb.mli @@ -23,6 +23,10 @@ * http://cs.unibo.it/helm/. *) + + (** THIS MODULE SHOULD BE USED ONLY BY CoercGraph **) + + (** XXX WARNING: non-reentrant *) type coerc_carr = Uri of UriManager.uri | Sort of Cic.sort | Term of Cic.term exception EqCarrNotImplemented of string Lazy.t @@ -31,8 +35,6 @@ val eq_carr: coerc_carr -> coerc_carr -> bool val coerc_carr_of_term: Cic.term -> coerc_carr val name_of_carr: coerc_carr -> string -val use_coercions: bool ref (** initial status is true *) - val to_list: unit -> (coerc_carr * coerc_carr * UriManager.uri) list @@ -43,6 +45,10 @@ val add_coercion: val remove_coercion: (coerc_carr * coerc_carr * UriManager.uri -> bool) -> unit -val find_coercion: +val find_coercion: (coerc_carr * coerc_carr -> bool) -> UriManager.uri list +val is_a_coercion: UriManager.uri -> bool +val get_carr: UriManager.uri -> coerc_carr * coerc_carr + + diff --git a/helm/ocaml/library/coercGraph.ml b/helm/ocaml/library/coercGraph.ml index 77c449e04..3862fcccc 100644 --- a/helm/ocaml/library/coercGraph.ml +++ b/helm/ocaml/library/coercGraph.ml @@ -156,7 +156,7 @@ let filter_duplicates l coercions = let term_of_carr = function | CoercDb.Uri u -> CicUtil.term_of_uri u - | CoercDb.Sort _ -> assert false + | CoercDb.Sort s -> Cic.Sort s | CoercDb.Term _ -> assert false (* given a new coercion uri from src to tgt returns @@ -167,49 +167,48 @@ let close_coercion_graph src tgt uri = let coercions = CoercDb.to_list () in let todo_list = get_closure_coercions src tgt uri coercions in let todo_list = filter_duplicates todo_list coercions in - let new_coercions, new_coercions_obj = - List.split ( - List.map ( - fun (src, l , tgt) -> - match l with - | [] -> assert false - | he :: tl -> - let first_step = - Cic.Constant ("", - Some (term_of_carr (CoercDb.Uri he)), Cic.Sort Cic.Prop, [], obj_attrs) - in - let o,u = - List.fold_left (fun (o,univ) coer -> - match o with - | Cic.Constant (_,Some c,_,[],_) -> - generate_composite_closure c (term_of_carr (CoercDb.Uri - coer)) univ - | _ -> assert false - ) (first_step, CicUniv.empty_ugraph) tl - in - let name_src = CoercDb.name_of_carr src in - let name_tgt = CoercDb.name_of_carr tgt in - let name = name_tgt ^ "_of_" ^ name_src in - let buri = UriManager.buri_of_uri uri in - let c_uri = - UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") - in - let named_obj = - match o with - | Cic.Constant (_,bo,ty,vl,attrs) -> - Cic.Constant (name,bo,ty,vl,attrs) + let new_coercions = + List.map ( + fun (src, l , tgt) -> + match l with + | [] -> assert false + | he :: tl -> + let first_step = + Cic.Constant ("", + Some (term_of_carr (CoercDb.Uri he)), + Cic.Sort Cic.Prop, [], obj_attrs) + in + let o,_ = + List.fold_left (fun (o,univ) coer -> + match o with + | Cic.Constant (_,Some c,_,[],_) -> + generate_composite_closure c (term_of_carr (CoercDb.Uri + coer)) univ | _ -> assert false - in - ((src,tgt,c_uri),(c_uri,named_obj,u)) - ) todo_list) + ) (first_step, CicUniv.empty_ugraph) tl + in + let name_src = CoercDb.name_of_carr src in + let name_tgt = CoercDb.name_of_carr tgt in + let name = name_tgt ^ "_of_" ^ name_src in + let buri = UriManager.buri_of_uri uri in + let c_uri = + UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") + in + let named_obj = + match o with + | Cic.Constant (_,bo,ty,vl,attrs) -> + Cic.Constant (name,bo,ty,vl,attrs) + | _ -> assert false + in + ((src,tgt,c_uri,named_obj)) + ) todo_list in - List.iter CoercDb.add_coercion (new_coercions @ [src,tgt,uri]); - new_coercions_obj + new_coercions ;; let coercion_hashtbl = UriManager.UriHashtbl.create 3 -let add_coercion ~basedir ~add_composites uri = +let add_coercion uri = let coer_ty,_ = CicTypeChecker.type_of_aux' [] [] (CicUtil.term_of_uri uri) CicUniv.empty_ugraph @@ -233,35 +232,47 @@ let add_coercion ~basedir ~add_composites uri = let src_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in let tgt_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in let new_coercions = close_coercion_graph src_uri tgt_uri uri in - let uris = ref [] in - if add_composites then - try - let lemmas = - List.fold_left - (fun lemmas (uri,o,_) -> - let lemmas' = LibrarySync.add_obj ~basedir uri o in - uris := uri :: !uris; - uri::lemmas'@lemmas - ) [] new_coercions; - in - UriManager.UriHashtbl.add coercion_hashtbl uri !uris; - lemmas - with - exn -> - List.iter LibrarySync.remove_obj !uris; - raise exn - else - [] + UriManager.UriHashtbl.add coercion_hashtbl uri + (List.map (fun (_,_,uri,_) -> uri) new_coercions); + CoercDb.add_coercion (src_uri,tgt_uri,uri); + List.iter + (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri)) + new_coercions; + List.map (fun (_,_,uri,o) -> uri,o) new_coercions + let remove_coercion uri = - let uris = try let res = UriManager.UriHashtbl.find coercion_hashtbl uri in UriManager.UriHashtbl.remove coercion_hashtbl uri; - res + CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq uri u); + List.iter + (fun u -> + CoercDb.remove_coercion + (fun (_,_,u1) -> UriManager.eq u u1)) + res; with - Not_found -> assert false - in - List.iter LibrarySync.remove_obj uris + Not_found -> () + +let remove_all () = + CoercDb.remove_coercion (fun (_,_,u1) -> true) +let is_a_coercion t = + try + let uri = CicUtil.uri_of_term t in + CoercDb.is_a_coercion uri + with Invalid_argument _ -> false + +let source_of t = + try + let uri = CicUtil.uri_of_term t in + term_of_carr (fst (CoercDb.get_carr uri)) + with Invalid_argument _ -> assert false (* t must be a coercion *) + +let target_of t = + try + let uri = CicUtil.uri_of_term t in + term_of_carr (snd (CoercDb.get_carr uri)) + with Invalid_argument _ -> assert false (* t must be a coercion *) + (* EOF *) diff --git a/helm/ocaml/library/coercGraph.mli b/helm/ocaml/library/coercGraph.mli index bd562414e..b21fb96be 100644 --- a/helm/ocaml/library/coercGraph.mli +++ b/helm/ocaml/library/coercGraph.mli @@ -32,10 +32,17 @@ type coercion_search_result = val look_for_coercion : Cic.term -> Cic.term -> coercion_search_result -(* it returns the list of composite coercions and their auxiliary lemmas *) +(* it returns the list of composite coercions *) (* composite coercions are always declared as such; they are added to the *) -(* library only on demand (i.e. not when processing a .moo) *) +(* CoercDb adding them to the library is left to the caller *) val add_coercion: - basedir:string -> add_composites:bool -> UriManager.uri -> UriManager.uri list + UriManager.uri -> + (UriManager.uri * Cic.obj) list val remove_coercion: UriManager.uri -> unit + +val is_a_coercion: Cic.term -> bool +val source_of: Cic.term -> Cic.term +val target_of: Cic.term -> Cic.term + +val remove_all: unit -> unit diff --git a/helm/ocaml/library/librarySync.ml b/helm/ocaml/library/librarySync.ml index e41316ec6..707b355b0 100644 --- a/helm/ocaml/library/librarySync.ml +++ b/helm/ocaml/library/librarySync.ml @@ -25,6 +25,82 @@ exception AlreadyDefined of UriManager.uri +let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29 + +let merge_coercions obj = + let module C = Cic in + let rec aux2 = (fun (u,t) -> u,aux t) + and aux = function + | C.Rel _ | C.Sort _ as t -> t + | C.Meta _ | C.Implicit _ -> assert false + | C.Cast (te,ty) -> C.Cast (aux te, aux ty) + | C.Prod (name,so,dest) -> + C.Prod (name, aux so, aux dest) + | C.Lambda (name,so,dest) -> + C.Lambda (name, aux so, aux dest) + | C.LetIn (name,so,dest) -> + C.LetIn (name, aux so, aux dest) + | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) as t when + CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 -> + let source_carr = CoercGraph.source_of c2 in + let tgt_carr = CoercGraph.target_of c1 in + (match CoercGraph.look_for_coercion source_carr tgt_carr + with + | CoercGraph.SomeCoercion c -> Cic.Appl [ c ; head ] + | _ -> assert false) (* the composite coercion must exist *) + | C.Appl l -> C.Appl (List.map aux l) + | C.Var (uri,exp_named_subst) -> + let exp_named_subst = List.map aux2 exp_named_subst in + C.Var (uri, exp_named_subst) + | C.Const (uri,exp_named_subst) -> + let exp_named_subst = List.map aux2 exp_named_subst in + C.Const (uri, exp_named_subst) + | C.MutInd (uri,tyno,exp_named_subst) -> + let exp_named_subst = List.map aux2 exp_named_subst in + C.MutInd (uri,tyno,exp_named_subst) + | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> + let exp_named_subst = List.map aux2 exp_named_subst in + C.MutConstruct (uri,tyno,consno,exp_named_subst) + | C.MutCase (uri,tyno,out,te,pl) -> + let pl = List.map aux pl in + C.MutCase (uri,tyno,aux out,aux te,pl) + | C.Fix (fno, fl) -> + let fl = List.map (fun (name,idx,ty,bo)->(name,idx,aux ty,aux bo)) fl in + C.Fix (fno, fl) + | C.CoFix (fno, fl) -> + let fl = List.map (fun (name,ty,bo) -> (name, aux ty, aux bo)) fl in + C.CoFix (fno, fl) + in + match obj with + | C.Constant (id, body, ty, params, attrs) -> + let body = + match body with + | None -> None + | Some body -> Some (aux body) + in + let ty = aux ty in + C.Constant (id, body, ty, params, attrs) + | C.Variable (name, body, ty, params, attrs) -> + let body = + match body with + | None -> None + | Some body -> Some (aux body) + in + let ty = aux ty in + C.Variable (name, body, ty, params, attrs) + | C.CurrentProof (_name, _conjectures, _body, _ty, _params, _attrs) -> + assert false + | C.InductiveDefinition (indtys, params, leftno, attrs) -> + let indtys = + List.map + (fun (name, ind, arity, cl) -> + let arity = aux arity in + let cl = List.map (fun (name, ty) -> (name,aux ty)) cl in + (name, ind, arity, cl)) + indtys + in + C.InductiveDefinition (indtys, params, leftno, attrs) + let uris_of_obj uri = let innertypesuri = UriManager.innertypesuri_of_uri uri in let bodyuri = UriManager.bodyuri_of_uri uri in @@ -93,6 +169,14 @@ let index_obj = profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri let add_single_obj uri obj ~basedir = + let obj = + if List.mem `Generated (CicUtil.attributes_of_obj obj) && + not (CoercGraph.is_a_coercion (Cic.Const (uri, []))) + then + merge_coercions obj + else + obj + in let dbd = LibraryDb.instance () in if CicEnvironment.in_library uri then raise (AlreadyDefined uri) @@ -137,7 +221,7 @@ let remove_single_obj uri = HExtlib.rmdir_descend (Filename.dirname file) with Http_getter_types.Key_not_found _ -> ()); ignore (LibraryDb.remove_uri uri); - CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri); + CoercGraph.remove_coercion uri; CicEnvironment.remove_obj uri) to_remove @@ -161,17 +245,28 @@ let generate_elimination_principles ~basedir uri = let generate_projections ~basedir uri fields = let uris = ref [] in - let projections = CicRecord.projections_of uri fields in + let projections = CicRecord.projections_of uri (List.map fst fields) in try - List.iter - (fun (uri, name, bo) -> + List.iter2 + (fun (uri, name, bo) (_name, coercion) -> try let ty, ugraph = CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in let attrs = [`Class `Projection; `Generated] in let obj = Cic.Constant (name,Some bo,ty,[],attrs) in + add_single_obj ~basedir uri obj; - uris := uri :: !uris + let composites = + if coercion then + (* this is _NOT_ the place for THIS!!! *) + (* MOO HANDLING IS MISSING *) + let toadd = CoercGraph.add_coercion uri in + List.iter (fun (uri,o) -> add_single_obj ~basedir uri o) toadd; + List.map fst toadd + else + [] + in + uris := uri :: composites @ !uris with CicTypeChecker.TypeCheckerFailure s -> HLog.message @@ -181,13 +276,12 @@ let generate_projections ~basedir uri fields = HLog.message ("Unable to create projection " ^ name ^ " because it requires " ^ depend) - ) projections; + ) projections fields; !uris with exn -> List.iter remove_single_obj !uris; raise exn -let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29 let add_obj uri obj ~basedir = add_single_obj uri obj ~basedir; diff --git a/helm/ocaml/library/librarySync.mli b/helm/ocaml/library/librarySync.mli index 89262e393..1400b081b 100644 --- a/helm/ocaml/library/librarySync.mli +++ b/helm/ocaml/library/librarySync.mli @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +exception AlreadyDefined of UriManager.uri + (* adds an object to the library together with all auxiliary lemmas on it *) (* (e.g. elimination principles, projections, etc.) *) (* it returns the list of the uris of the auxiliary lemmas generated *) diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend index d667574fa..9ff04ffec 100644 --- a/helm/ocaml/tactics/.depend +++ b/helm/ocaml/tactics/.depend @@ -63,10 +63,10 @@ introductionTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \ introductionTactics.cmi eliminationTactics.cmo: tacticals.cmi proofEngineTypes.cmi \ proofEngineStructuralRules.cmi proofEngineHelpers.cmi \ - primitiveTactics.cmi metadataQuery.cmi eliminationTactics.cmi + primitiveTactics.cmi eliminationTactics.cmi eliminationTactics.cmx: tacticals.cmx proofEngineTypes.cmx \ proofEngineStructuralRules.cmx proofEngineHelpers.cmx \ - primitiveTactics.cmx metadataQuery.cmx eliminationTactics.cmi + primitiveTactics.cmx eliminationTactics.cmi negationTactics.cmo: variousTactics.cmi tacticals.cmi proofEngineTypes.cmi \ primitiveTactics.cmi eliminationTactics.cmi negationTactics.cmi negationTactics.cmx: variousTactics.cmx tacticals.cmx proofEngineTypes.cmx \ @@ -99,10 +99,10 @@ fourierR.cmx: tacticals.cmx ring.cmx reductionTactics.cmx \ fourier.cmx equalityTactics.cmx fourierR.cmi fwdSimplTactic.cmo: tacticals.cmi proofEngineTypes.cmi \ proofEngineStructuralRules.cmi proofEngineHelpers.cmi \ - primitiveTactics.cmi metadataQuery.cmi fwdSimplTactic.cmi + primitiveTactics.cmi fwdSimplTactic.cmi fwdSimplTactic.cmx: tacticals.cmx proofEngineTypes.cmx \ proofEngineStructuralRules.cmx proofEngineHelpers.cmx \ - primitiveTactics.cmx metadataQuery.cmx fwdSimplTactic.cmi + primitiveTactics.cmx fwdSimplTactic.cmi history.cmo: history.cmi history.cmx: history.cmi statefulProofEngine.cmo: proofEngineTypes.cmi history.cmi \ diff --git a/helm/ocaml/tactics/doc/body.tex b/helm/ocaml/tactics/doc/body.tex index 424dee225..8b7bbc9b0 100644 --- a/helm/ocaml/tactics/doc/body.tex +++ b/helm/ocaml/tactics/doc/body.tex @@ -17,13 +17,13 @@ like Coq, Isabelle, PhoX, LEGO, and many more. Other system specific GUIs exist but share the same design, understanding it and they way such GUIs are operated is relevant to our discussion. -\begin{figure}[ht] - \begin{center} - \resizebox{\textwidth}{!}{\includegraphics{pics/pg-coq-screenshot}} - \caption{Proof General: a generic interface for proof assistants} - \label{fig:proofgeneral} - \end{center} -\end{figure} +%\begin{figure}[ht] +% \begin{center} +% \includegraphic{pics/pg-coq-screenshot} +% \caption{Proof General: a generic interface for proof assistants} +% \label{fig:proofgeneral} +% \end{center} +%\end{figure} % - modo di lavorare @@ -52,42 +52,42 @@ minus with natural plus, along with its proof (line numbers have been added for the sake of presentation) as it can be found in the standard library of the \MATITA{} proof assistant: -\begin{example} -\begin{Verbatim} -theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p). - intros. - cut (m+p \le n \or m+p \nleq n). - elim Hcut. - symmetry. - apply plus_to_minus. - rewrite > assoc_plus. - rewrite > (sym_plus p). - rewrite < plus_minus_m_m. - rewrite > sym_plus. - rewrite < plus_minus_m_m. - reflexivity. - apply (trans_le ? (m+p)). - rewrite < sym_plus. - apply le_plus_n. - assumption. - apply le_plus_to_minus_r. - rewrite > sym_plus. - assumption. - rewrite > (eq_minus_n_m_O n (m+p)). - rewrite > (eq_minus_n_m_O (n-m) p). - reflexivity. - apply le_plus_to_minus. - apply lt_to_le. - rewrite < sym_plus. - apply not_le_to_lt. - assumption. - apply lt_to_le. - apply not_le_to_lt. - assumption. - apply (decidable_le (m+p) n). -qed. -\end{Verbatim} -\end{example} +%\begin{example} +%\begin{Verbatim} +%theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p). +% intros. +% cut (m+p \le n \or m+p \nleq n). +% elim Hcut. +% symmetry. +% apply plus_to_minus. +% rewrite > assoc_plus. +% rewrite > (sym_plus p). +% rewrite < plus_minus_m_m. +% rewrite > sym_plus. +% rewrite < plus_minus_m_m. +% reflexivity. +% apply (trans_le ? (m+p)). +% rewrite < sym_plus. +% apply le_plus_n. +% assumption. +% apply le_plus_to_minus_r. +% rewrite > sym_plus. +% assumption. +% rewrite > (eq_minus_n_m_O n (m+p)). +% rewrite > (eq_minus_n_m_O (n-m) p). +% reflexivity. +% apply le_plus_to_minus. +% apply lt_to_le. +% rewrite < sym_plus. +% apply not_le_to_lt. +% assumption. +% apply lt_to_le. +% apply not_le_to_lt. +% assumption. +% apply (decidable_le (m+p) n). +%qed. +%\end{Verbatim} +%\end{example} The script snippet is made of 32 statements, one per line (but this is not a requirement of the \MATITA{} script language, namely \emph{Grafite}). The first @@ -103,13 +103,13 @@ replaying) the above script, the user may position it at the end of any line, having feedback about the status of the proof in that point. See for example Fig.~\ref{fig:matita} where an intermediate proof status is shown. -\begin{figure}[ht] - \begin{center} - \resizebox{\textwidth}{!}{\includegraphics{matita_screenshot}} - \caption{Matita: ongoing proof} - \label{fig:matita} - \end{center} -\end{figure} +%\begin{figure}[ht] +% \begin{center} +% \includegraphic{matita_screenshot} +% \caption{Matita: ongoing proof} +% \label{fig:matita} +% \end{center} +%\end{figure} % - script: sorgenti di un linguaggio imperativo, oggetti la loro semantica % - script = sequenza di comandi @@ -193,11 +193,11 @@ Finally, the branching constructs \texttt{[}, \texttt{|}, and \texttt{]} enable proof structuring. Consider for example an alternative, branching based, version of the example above: -\begin{example} -\begin{Verbatim} -... -\end{Verbatim} -\end{example} +%\begin{example} +%\begin{Verbatim} +%... +%\end{Verbatim} +%\end{example} Tactic applications are the same of the previous version of the script, but branching tacticals are used. The above version is highly more readable and diff --git a/helm/ocaml/tactics/doc/main.tex b/helm/ocaml/tactics/doc/main.tex index 00208b0c2..06952d61c 100644 --- a/helm/ocaml/tactics/doc/main.tex +++ b/helm/ocaml/tactics/doc/main.tex @@ -4,6 +4,7 @@ \usepackage{pifont} \usepackage{semantic} \usepackage{stmaryrd} +\usepackage{graphicx} \newcommand{\MATITA}{\ding{46}\textsf{\textbf{Matita}}} -- 2.39.2