From c5d5bf37b1e4c4b9b499ed2cbfe27cf2ec181944 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 23 Apr 2004 10:37:00 +0000 Subject: [PATCH] Universes introduction --- helm/ocaml/cic/.depend | 8 +- helm/ocaml/cic/Makefile | 2 +- helm/ocaml/cic/cic.ml | 2 +- helm/ocaml/cic/cicParser3.ml | 2 +- helm/ocaml/cic/cicUniv.ml | 345 ++++++++++++++++++ helm/ocaml/cic/cicUniv.mli | 39 ++ helm/ocaml/cic_disambiguation/disambiguate.ml | 2 +- helm/ocaml/cic_omdoc/cic2acic.ml | 7 +- helm/ocaml/cic_omdoc/doubleTypeInference.ml | 23 +- helm/ocaml/cic_proof_checking/cicPp.ml | 2 +- .../cic_proof_checking/cicReductionMachine.ml | 15 +- .../cic_proof_checking/cicReductionNaif.ml | 13 +- .../cic_proof_checking/cicTypeChecker.ml | 38 +- .../cic_textual_parser/cicTextualParser.mly | 14 +- helm/ocaml/cic_transformations/.depend | 4 +- helm/ocaml/cic_transformations/acic2Ast.ml | 2 +- helm/ocaml/cic_transformations/cic2Xml.ml | 2 +- .../content_expressions.ml | 2 +- helm/ocaml/cic_unification/cicMkImplicit.ml | 20 +- helm/ocaml/cic_unification/cicRefine.ml | 24 +- helm/ocaml/cic_unification/cicUnification.ml | 88 +++-- helm/ocaml/getter/.depend | 28 +- .../ocaml/mathql_generator/cGSearchPattern.ml | 2 +- helm/ocaml/mathql_interpreter/.depend | 2 +- helm/ocaml/tactics/.depend | 4 +- helm/ocaml/tactics/primitiveTactics.ml | 14 +- .../texCicTextualParser.mly | 14 +- 27 files changed, 612 insertions(+), 106 deletions(-) create mode 100644 helm/ocaml/cic/cicUniv.ml create mode 100644 helm/ocaml/cic/cicUniv.mli diff --git a/helm/ocaml/cic/.depend b/helm/ocaml/cic/.depend index 83d250bae..21bc8d14a 100644 --- a/helm/ocaml/cic/.depend +++ b/helm/ocaml/cic/.depend @@ -4,10 +4,14 @@ cicParser2.cmi: cic.cmo cicParser3.cmi cicParser.cmi: cic.cmo cicUtil.cmi: cic.cmo helmLibraryObjects.cmi: cic.cmo +cic.cmo: cicUniv.cmi +cic.cmx: cicUniv.cmx +cicUniv.cmo: cicUniv.cmi +cicUniv.cmx: cicUniv.cmi deannotate.cmo: cic.cmo deannotate.cmi deannotate.cmx: cic.cmx deannotate.cmi -cicParser3.cmo: cic.cmo cicParser3.cmi -cicParser3.cmx: cic.cmx cicParser3.cmi +cicParser3.cmo: cic.cmo cicUniv.cmi cicParser3.cmi +cicParser3.cmx: cic.cmx cicUniv.cmx cicParser3.cmi cicParser2.cmo: cic.cmo cicParser3.cmi cicParser2.cmi cicParser2.cmx: cic.cmx cicParser3.cmx cicParser2.cmi cicParser.cmo: cicParser2.cmi cicParser3.cmi deannotate.cmi cicParser.cmi diff --git a/helm/ocaml/cic/Makefile b/helm/ocaml/cic/Makefile index f7933c605..8fb3c7c0c 100644 --- a/helm/ocaml/cic/Makefile +++ b/helm/ocaml/cic/Makefile @@ -3,7 +3,7 @@ REQUIRES = helm-urimanager helm-pxp PREDICATES = INTERFACE_FILES = \ - deannotate.mli cicParser3.mli cicParser2.mli cicParser.mli cicUtil.mli helmLibraryObjects.mli + cicUniv.mli deannotate.mli cicParser3.mli cicParser2.mli cicParser.mli cicUtil.mli helmLibraryObjects.mli IMPLEMENTATION_FILES = \ cic.ml $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = cic.ml cic.cmi diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml index 55a338b3f..f9e99260d 100644 --- a/helm/ocaml/cic/cic.ml +++ b/helm/ocaml/cic/cic.ml @@ -52,7 +52,7 @@ type anntarget = and sort = Prop | Set - | Type + | Type of CicUniv.universe | CProp and name = Name of string diff --git a/helm/ocaml/cic/cicParser3.ml b/helm/ocaml/cic/cicParser3.ml index 121f36453..8e6d276d5 100644 --- a/helm/ocaml/cic/cicParser3.ml +++ b/helm/ocaml/cic/cicParser3.ml @@ -53,7 +53,7 @@ let cic_sort_of_xml_attr = function Pxp_types.Value "Prop" -> Cic.Prop | Pxp_types.Value "Set" -> Cic.Set - | Pxp_types.Value "Type" -> Cic.Type + | Pxp_types.Value "Type" -> Cic.Type (CicUniv.fresh ()) (* TASSI: sure? *) | _ -> raise (IllFormedXml 2) let int_of_xml_attr = diff --git a/helm/ocaml/cic/cicUniv.ml b/helm/ocaml/cic/cicUniv.ml new file mode 100644 index 000000000..d76fde47a --- /dev/null +++ b/helm/ocaml/cic/cicUniv.ml @@ -0,0 +1,345 @@ +(* 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/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Enrico Tassi *) +(* 23/04/2004 *) +(* *) +(* This module implements the aciclic graph of universes. *) +(* *) +(******************************************************************************) + +(* + + todo: + - in add_eq there is probably no need of add_gt, simple @ the gt lists + - the problem of duplicates in the 1steg gt/ge list if two of them are + add_eq may be "fixed" in some ways: + - lazy, do nothing on add_eq and eventually update the ge list + on closure + - add a check_duplicates_after_eq function called by add_eq + - do something like rmap, add a list of canonical that point to us + so when we collapse we have the list of the canonical we may update + - don't use failure but another exception + +*) + +(* ************************************************************************** *) +(* TYPES *) +(* ************************************************************************** *) +type universe = int + +type canonical_repr = { + mutable ge:universe list; + mutable gt:universe list; + (* since we collapse we may need the reverse map *) + mutable eq:universe list; + (* the canonical representer *) + u:universe +} + +module UniverseType = struct + type t = universe + let compare = Pervasives.compare +end + +module MapUC = Map.Make(UniverseType) + +(* ************************************************************************** *) +(* Globals *) +(* ************************************************************************** *) + +let map = ref MapUC.empty +let used = ref (-1) + +(* ************************************************************************** *) +(* Helpers *) +(* ************************************************************************** *) + +(* create a canonical for [u] *) +let mk_canonical u = + {u = u ; gt = [] ; ge = [] ; eq = [u] } + +(* give a new universe *) +let fresh () = + used := !used + 1; + map := MapUC.add !used (mk_canonical !used) !map; + !used + +let reset () = + map := MapUC.empty; + used := -1 + +(* ************************************************************************** *) +(* Pretty printing *) +(* ************************************************************************** *) +(* pp *) +let string_of_universe = string_of_int + +(* pp *) +let canonical_to_string c = + let s_gt = + List.fold_left (fun s u -> s ^ (string_of_universe u) ^ " ") "" c.gt in + let s_ge = + List.fold_left (fun s u -> s ^ (string_of_universe u) ^ " ") "" c.ge in + let s_eq = + List.fold_left (fun s u -> s ^ (string_of_universe u) ^ " ") "" c.eq in + let s_u = (string_of_universe c.u) in + "{ u:" ^ s_u ^ " ; gt:" ^ s_gt ^ " ; ge:" ^ s_ge ^ " ; eq: " ^ s_eq ^ "}" + +(* print the content of map *) +let print_map () = + MapUC.iter (fun u c -> + prerr_endline + (" " ^ (string_of_universe u) ^ " -> " ^ (canonical_to_string c))) + !map; + prerr_endline "" + +(* ************************************************************************** *) +(* The way we fail *) +(* ************************************************************************** *) +(* we are doing bad *) +let error s = + (*prerr_endline " ======= Universe Inconsistency ========="; + print_map ();*) + prerr_endline (" " ^ s ^ "\n"); + failwith s + +(* ************************************************************************** *) +(* The real code *) +(* ************************************************************************** *) +(* <--------> *) + +(* the canonical representer of the [u] equaliti class *) +let repr u = + try + MapUC.find u !map + with + Not_found -> error ("map inconsistency, unbound " ^ (string_of_universe u)) + +(* all the nodes we can ifer in the ge list of u *) +let close_ge u = + let repr_u = repr u in + let rec close_ge_aux tofollow bag = + match tofollow with + [] -> bag + | v::tl -> let repr_v = repr v in + if List.mem repr_v bag then (* avoid loops *) + (close_ge_aux tl bag ) + else + (close_ge_aux (tl @ repr_v.ge) (repr_v::bag)) + (* we assume that v==u -> v \notin (repr u).ge *) + in + close_ge_aux repr_u.ge [] + +(* all the nodes we can ifer in the gt list of u, + we must follow bot gt and ge arcs, but we must put in bag only + the nodes that have a gt in theys path +*) +let close_gt u = + let repr_u = repr u in + let rec close_gt_aux bag todo inspected = + (*print_all bag todo;Unix.sleep 1;*) + match todo with + [],[] -> bag + | [],p::may -> let repr_p = repr p in + if List.mem repr_p.u inspected then (* avoid loops *) + close_gt_aux bag ([],may) inspected + else + close_gt_aux bag (repr_p.gt,repr_p.ge @ may) + (repr_p.u::inspected) + | s::secure,may -> let repr_s = repr s in + if List.mem repr_s.u inspected then (* avoid loops *) + if List.mem repr_s bag then + close_gt_aux bag (secure,may) inspected + else + (* even if we ave already inspected the node, now + it is in the secure list so we want it in the bag + *) + close_gt_aux (repr_s::bag) (secure,may) inspected + else + close_gt_aux ((repr_s)::bag) + (repr_s.gt @ repr_s.ge,may) (repr_s.u::inspected) + in + close_gt_aux [] (repr_u.gt,repr_u.ge) [] + +(* when we add an eq we have to change the mapping of u to c*) +let remap u c = + let repr_u = repr u in + List.iter (fun u' -> if u <> u' then map := MapUC.remove u' !map) repr_u.eq; + List.iter (fun u' -> map := MapUC.add u' c !map) repr_u.eq + +(* we suspect that u and v are connected by a == implyed by two >= *) +let rec collapse u v = + let repr_u = repr u in + let repr_v = repr v in + let ge_v = close_ge v in + let ge_u = close_ge u in + if List.mem repr_u ge_v && List.mem repr_v ge_u then + add_eq u v + +(* we have to add u == v *) +and add_eq u v = + let repr_u = repr u in + let repr_v = repr v in + (* if we already have u == v then do nothing *) + if repr_u = repr_v then + () + else + (* if we already have v > u then fail *) + let gt_v = close_gt v in + if List.mem repr_u gt_v then + error ("Asking for " ^ (string_of_universe u) ^ " == " ^ + (string_of_universe v) ^ " but " ^ + (string_of_universe v) ^ " > " ^ (string_of_universe u)) + else + (* if we already have u > v then fail *) + let gt_u = close_gt u in + if List.mem repr_v gt_u then + error ("Asking for " ^ (string_of_universe u) ^ " == " ^ + (string_of_universe v) ^ " but " ^ + (string_of_universe u) ^ " > " ^ (string_of_universe v)) + else + (* add the inherited > constraints *) + List.iter (fun v -> add_gt u v ) (*gt_v*) repr_v.gt; + (* add the inherited >= constraints *) + (* close_ge assumes that v==u -> v \notin (repr u).ge *) + repr_u.ge <- List.filter (fun x -> x <> u && x <> v) + (repr_v.ge @ repr_u.ge); + (* mege the eq list, we assume they are disjuncted *) + repr_u.eq <- repr_u.eq @ repr_v.eq; + (* we have to remap all node represented by repr_v to repr_u *) + remap v repr_u; + (* FIXME: not sure this is what we have to do + think more to the list of suspected cicles + *) + List.iter (fun x -> collapse u x) repr_u.ge + +(* we have to add u >= v *) +and add_ge u v = + let repr_u = repr u in + let repr_v = repr v in + (* if we already have u == v then do nothing *) + if repr_u = repr_v then + () + else + (* if we already have v > u then fail *) + let gt = close_gt v in + if List.memq repr_u gt then + error ("Asking for " ^ (string_of_universe u) ^ " >= " ^ + (string_of_universe v) ^ " but " ^ + (string_of_universe v) ^ " > " ^ (string_of_universe u)) + else + (* it is now safe to add u >= v *) + repr_u.ge <- v::repr_u.ge; + (* but we may have introduced a cicle *) + collapse u v (* FIXME: not sure it is from u to v, think more. *) + +(* we have to add u > v *) +and add_gt u v = + let repr_u = repr u in + let repr_v = repr v in + (* if we already have u == v then fail *) + if repr_u = repr_v then + error ("Asking for " ^ (string_of_universe u) ^ " > " ^ + (string_of_universe v) ^ " but " ^ + (string_of_universe u) ^ " == " ^ (string_of_universe v)) + else + (* if we already have u > v do nothing *) + let gt_u = close_gt u in + if List.memq repr_v gt_u then + () + else + (* if we already have v > u then fail *) + let gt = close_gt v in + if List.memq repr_u gt then + error ("Asking for " ^ (string_of_universe u) ^ " > " ^ + (string_of_universe v) ^ " but " ^ + (string_of_universe v) ^ " > " ^ (string_of_universe u)) + else + (* if we already have v >= u then fail *) + let ge = close_ge v in + if List.memq repr_u ge then + error ("Asking for " ^ (string_of_universe u) ^ " > " ^ + (string_of_universe v) ^ " but " ^ + (string_of_universe v) ^ " >= " ^ (string_of_universe u)) + else + (* it is safe to add u > v *) + repr_u.gt <- v::repr_u.gt + +let add_gt u v = + try + add_gt u v; true + with + exn -> false + +let add_ge u v = + try + add_ge u v; true + with + exn -> false + +let add_eq u v = + try + add_eq u v; true + with + exn -> false + +(* <--------> *) + +(* ************************************************************************** *) +(* To make tests *) +(* ************************************************************************** *) + +(* +let check_status_eq l = + let s = List.fold_left (fun s u -> s^(string_of_universe u) ^ ";") "" l in + let repr_u = repr (List.hd l) in + let rec check_status_eq_aux c = + match c with + [] -> print_endline (" Result check_status_eq["^s^"] = OK");true + | u::tl -> if repr u != repr_u then + (print_endline (" Result check_status_eq["^s^"] = FAILED"); + print_endline ((string_of_universe u) ^ " != " ^ + (string_of_universe repr_u.u)); + print_map ();false) + else + check_status_eq_aux tl + in + check_status_eq_aux (List.tl l) +*) + +(* ************************************************************************** *) +(* Fake implementation *) +(* ************************************************************************** *) + +(* <--------> * +let add_ge u v = true +let add_gt u v = true +let add_eq u v = true +* <--------> *) diff --git a/helm/ocaml/cic/cicUniv.mli b/helm/ocaml/cic/cicUniv.mli new file mode 100644 index 000000000..d7eb7dc41 --- /dev/null +++ b/helm/ocaml/cic/cicUniv.mli @@ -0,0 +1,39 @@ +(* Copyright (C) 2004, 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://helm.cs.unibo.it/ + *) + +type universe +val fresh: unit -> universe +val add_eq: universe -> universe -> bool +val add_ge: universe -> universe -> bool +val add_gt: universe -> universe -> bool + +(* +val string_of_universe: universe -> string +val print_map: unit -> unit +*) + +val reset: unit -> unit + +(* val check_status_eq: universe list -> bool *) diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index b09f0a8ef..139a6417a 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -257,7 +257,7 @@ let interpretate ~context ~env ast = Cic.Meta (index, cic_subst) | CicAst.Sort `Prop -> Cic.Sort Cic.Prop | CicAst.Sort `Set -> Cic.Sort Cic.Set - | CicAst.Sort `Type -> Cic.Sort Cic.Type + | CicAst.Sort `Type -> Cic.Sort (Cic.Type (CicUniv.fresh())) (* TASSI *) | CicAst.Sort `CProp -> Cic.Sort Cic.CProp | CicAst.Symbol (symbol, instance) -> resolve env (Symbol (symbol, instance)) () diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml index bf686ac4e..37e56406e 100644 --- a/helm/ocaml/cic_omdoc/cic2acic.ml +++ b/helm/ocaml/cic_omdoc/cic2acic.ml @@ -108,7 +108,7 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts match CicReduction.whd context t with C.Sort C.Prop -> "Prop" | C.Sort C.Set -> "Set" - | C.Sort C.Type -> "Type" + | C.Sort (C.Type _) -> "Type" (* TASSI OK*) | C.Sort C.CProp -> "CProp" | C.Meta _ -> prerr_endline "Cic2acic: string_of_sort applied to a meta" ; @@ -134,7 +134,7 @@ prerr_endline "Cic2acic: string_of_sort applied to a meta" ; {D.synthesized = (***CSC: patch per provare i tempi CicReduction.whd context (xxx_type_of_aux' metasenv context tt) ; *) -Cic.Sort Cic.Type ; +Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *) D.expected = None} in incr number_new_type_of_aux' ; @@ -162,7 +162,8 @@ Cic.Sort Cic.Type ; with Not_found -> (* l'inner-type non e' nella tabella ==> sort <> Prop *) (* CSC: Type or Set? I can not tell *) - None,Cic.Sort Cic.Type,"Type",false + None,Cic.Sort (Cic.Type (CicUniv.fresh())),"Type",false + (* TASSI non dovrebbe fare danni *) (* *) in let add_inner_type id = diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml index 3c6f4129a..441d7c9a9 100644 --- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml +++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml @@ -403,7 +403,13 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = in (* Checks suppressed *) CicSubstitution.lift_meta l ty - | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *) + | C.Sort (C.Type t) -> (* TASSI: CONSTRAINT *) + let t' = CicUniv.fresh() in + if not (CicUniv.add_gt t' t ) then + assert false (* t' is fresh! an error in CicUniv *) + else + C.Sort (C.Type t') + | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())) (* TASSI: CONSTRAINT *) | C.Implicit _ -> raise (Impossible 21) | C.Cast (te,ty) -> (* Let's visit all the subterms that will not be visited later *) @@ -668,10 +674,19 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = let t1' = CicReduction.whd context t1 in let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in match (t1', t2') with - (C.Sort s1, C.Sort s2) - when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *) + (C.Sort _, C.Sort s2) + when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> + (* different from Coq manual!!! *) C.Sort s2 - | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *) + | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> + (* TASSI: CONSRTAINTS: the same in cictypechecker,cicrefine *) + let t' = CicUniv.fresh() in + if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then + assert false ; (* not possible, error in CicUniv *) + C.Sort (C.Type t') + | (C.Sort _,C.Sort (C.Type t1)) -> + (* TASSI: CONSRTAINTS: the same in cictypechecker,cicrefine *) + C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *) | (C.Meta _, C.Sort _) -> t2' | (C.Meta _, (C.Meta (_,_) as t)) | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t -> diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml index b0e7d64ed..8172b47f7 100644 --- a/helm/ocaml/cic_proof_checking/cicPp.ml +++ b/helm/ocaml/cic_proof_checking/cicPp.ml @@ -85,7 +85,7 @@ let rec pp t l = (match s with C.Prop -> "Prop" | C.Set -> "Set" - | C.Type -> "Type" + | C.Type _ -> "Type" (* TASSI: universe is not explicit *) | C.CProp -> "CProp" ) | C.Implicit _ -> "?" diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml index 4ef3ce940..e963ddce9 100644 --- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml +++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml @@ -802,10 +802,17 @@ let are_convertible = | _,None -> true | Some t1',Some t2' -> aux test_equality_only context t1' t2' ) true l1 l2 - | (C.Sort s1, C.Sort s2) when - s1 = s2 || (not test_equality_only) && s2 = C.Type - -> true - | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> + (* TASSI: CONSTRAINTS *) + | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only -> + CicUniv.add_eq t2 t1 + (* TASSI: CONSTRAINTS *) + | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> + CicUniv.add_ge t2 t1 + (* TASSI: CONSTRAINTS *) + | (C.Sort s1, C.Sort (C.Type _)) -> not test_equality_only + (* TASSI: CONSTRAINTS *) + | (C.Sort s1, C.Sort s2) -> s1 = s2 + | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> aux true context s1 s2 && aux test_equality_only ((Some (name1, (C.Decl s1)))::context) t1 t2 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) -> diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml index 033614eea..95f24ebf3 100644 --- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml +++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml @@ -215,9 +215,16 @@ let are_convertible = | _,None -> true | Some t1',Some t2' -> aux test_equality_only context t1' t2' ) true l1 l2 - | (C.Sort s1, C.Sort s2) when - s1 = s2 || (not test_equality_only) && s2 = C.Type - -> true + (* TASSI: CONSTRAINTS *) + | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only -> + CicUniv.add_eq t2 t1 + (* TASSI: CONSTRAINTS *) + | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> + CicUniv.add_ge t2 t1 + (* TASSI: CONSTRAINTS *) + | (C.Sort s1, C.Sort (C.Type _)) -> not test_equality_only + (* TASSI: CONSTRAINTS *) + | (C.Sort s1, C.Sort s2) -> s1 = s2 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> aux true context s1 s2 && aux test_equality_only ((Some (name1, (C.Decl s1)))::context) t1 t2 diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 04b769b5c..36bfb28b1 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -1174,7 +1174,8 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 = | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true | (C.Sort C.Prop, C.Sort C.Set) | (C.Sort C.Prop, C.Sort C.CProp) - | (C.Sort C.Prop, C.Sort C.Type) when need_dummy -> + | (C.Sort C.Prop, C.Sort (C.Type _) ) when need_dummy -> + (* TASSI: da verificare *) (*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *) (match CicEnvironment.get_obj uri with C.InductiveDefinition (itl,_,_) -> @@ -1191,7 +1192,8 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 = | (C.Sort C.Set, C.Sort C.CProp) when need_dummy -> true | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true - | ((C.Sort C.Set, C.Sort C.Type) | (C.Sort C.CProp, C.Sort C.Type)) + | ((C.Sort C.Set, C.Sort (C.Type _)) | (C.Sort C.CProp, C.Sort (C.Type _))) + (* TASSI: da verificare *) when need_dummy -> (match CicEnvironment.get_obj uri with C.InductiveDefinition (itl,_,paramsno) -> @@ -1205,7 +1207,8 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 = raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri)) ) - | (C.Sort C.Type, C.Sort _) when need_dummy -> true + | (C.Sort (C.Type _), C.Sort _) when need_dummy -> true + (* TASSI: da verificare *) | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy -> let res = CicReduction.are_convertible context so ind in @@ -1234,7 +1237,8 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 = C.Sort C.Prop | C.Sort C.Set -> true | C.Sort C.CProp -> true - | C.Sort C.Type -> + | C.Sort (C.Type _) -> + (* TASSI: da verificare *) (match CicEnvironment.get_obj uri with C.InductiveDefinition (itl,_,paramsno) -> let (_,_,_,cl) = List.nth itl i in @@ -1251,7 +1255,8 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 = ) | _ -> raise (AssertFailure "19") ) - | (C.Sort C.Type, C.Prod (_,so,_)) when not need_dummy -> + | (C.Sort (C.Type _), C.Prod (_,so,_)) when not need_dummy -> + (* TASSI: da verificare *) CicReduction.are_convertible context so ind | (_,_) -> false @@ -1357,7 +1362,15 @@ and type_of_aux' metasenv context t = let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in check_metasenv_consistency metasenv context canonical_context l; CicSubstitution.lift_meta l ty - | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *) + (* TASSI: CONSTRAINTS *) + | C.Sort (C.Type t) -> + let t' = CicUniv.fresh() in + if not (CicUniv.add_gt t' t ) then + assert false (* t' is fresh! an error in CicUniv *) + else + C.Sort (C.Type t') + (* TASSI: CONSTRAINTS *) + | C.Sort s -> C.Sort (C.Type (CicUniv.fresh ())) | C.Implicit _ -> raise (AssertFailure "21") | C.Cast (te,ty) as t -> let _ = type_of_aux context ty in @@ -1646,9 +1659,18 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^ let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in match (t1', t2') with (C.Sort s1, C.Sort s2) - when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *) + when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> + (* different from Coq manual!!! *) C.Sort s2 - | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *) + | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> + (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *) + let t' = CicUniv.fresh() in + if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then + assert false ; (* not possible, error in CicUniv *) + C.Sort (C.Type t') + | (C.Sort _,C.Sort (C.Type t1)) -> + (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *) + C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *) | (C.Meta _, C.Sort _) -> t2' | (C.Meta _, (C.Meta (_,_) as t)) | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t -> diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly index 84e0f0ee5..a869bc068 100644 --- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly +++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly @@ -135,13 +135,15 @@ ;; let mk_implicit () = + let newuniv = CicUniv.fresh () in + (* TASSI: what is an implicit? *) let newmeta = new_meta () in let new_canonical_context = [] in let irl = identity_relocation_list_for_metavariable new_canonical_context in CicTextualParser0.metasenv := - [newmeta, new_canonical_context, Sort Type ; + [newmeta, new_canonical_context, Sort (Type newuniv); newmeta+1, new_canonical_context, Meta (newmeta,irl); newmeta+2, new_canonical_context, Meta (newmeta+1,irl) ] @ !CicTextualParser0.metasenv ; @@ -288,7 +290,7 @@ expr2: { mk_implicit () } | SET { [], function _ -> Sort Set } | PROP { [], function _ -> Sort Prop } - | TYPE { [], function _ -> Sort Type } + | TYPE { [], function _ -> Sort (Type (CicUniv.fresh ())) (* TASSI: ?? *)} | CPROP { [], function _ -> Sort CProp } | LPAREN expr CAST expr RPAREN { let dom1,mk_expr1 = $2 in @@ -425,12 +427,14 @@ pihead: | PROD ID DOT { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders; let newmeta = new_meta () in + let newuniv = CicUniv.fresh () in let new_canonical_context = [] in let irl = identity_relocation_list_for_metavariable new_canonical_context in CicTextualParser0.metasenv := - [newmeta, new_canonical_context, Sort Type ; + [newmeta, new_canonical_context, Sort (Type newuniv); + (* TASSI: ?? *) newmeta+1, new_canonical_context, Meta (newmeta,irl) ] @ !CicTextualParser0.metasenv ; Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl)) @@ -445,12 +449,14 @@ lambdahead: | LAMBDA ID DOT { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders; let newmeta = new_meta () in + let newuniv = CicUniv.fresh () in let new_canonical_context = [] in let irl = identity_relocation_list_for_metavariable new_canonical_context in CicTextualParser0.metasenv := - [newmeta, new_canonical_context, Sort Type ; + [newmeta, new_canonical_context, Sort (Type newuniv); + (* TASSI: ?? *) newmeta+1, new_canonical_context, Meta (newmeta,irl) ] @ !CicTextualParser0.metasenv ; Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl)) diff --git a/helm/ocaml/cic_transformations/.depend b/helm/ocaml/cic_transformations/.depend index 7506b4d52..7f03ceb1a 100644 --- a/helm/ocaml/cic_transformations/.depend +++ b/helm/ocaml/cic_transformations/.depend @@ -11,8 +11,6 @@ boxPp.cmi: box.cmi cicAst.cmo tacticAst2Box.cmi: box.cmi cicAst.cmo tacticAst.cmo tacticAst.cmo: cicAst.cmo tacticAst.cmx: cicAst.cmx -commandAst.cmo: cicAst.cmo cicAstPp.cmi tacticAst.cmo tacticAstPp.cmi -commandAst.cmx: cicAst.cmx cicAstPp.cmx tacticAst.cmx tacticAstPp.cmx box.cmo: box.cmi box.cmx: box.cmi contentTable.cmo: cicAst.cmo contentTable.cmi @@ -65,3 +63,5 @@ tacticAst2Box.cmo: ast2pres.cmi box.cmi boxPp.cmi cicAstPp.cmi tacticAst.cmo \ tacticAstPp.cmi tacticAst2Box.cmi tacticAst2Box.cmx: ast2pres.cmx box.cmx boxPp.cmx cicAstPp.cmx tacticAst.cmx \ tacticAstPp.cmx tacticAst2Box.cmi +commandAst.cmo: cicAst.cmo cicAstPp.cmi tacticAst.cmo tacticAstPp.cmi +commandAst.cmx: cicAst.cmx cicAstPp.cmx tacticAst.cmx tacticAstPp.cmx diff --git a/helm/ocaml/cic_transformations/acic2Ast.ml b/helm/ocaml/cic_transformations/acic2Ast.ml index e51e9c0a4..1bc76ebb8 100644 --- a/helm/ocaml/cic_transformations/acic2Ast.ml +++ b/helm/ocaml/cic_transformations/acic2Ast.ml @@ -78,7 +78,7 @@ let ast_of_acic ids_to_inner_sorts ids_to_uris acic = | Cic.AMeta (id,n,l) -> idref id (Ast.Meta (n, astcontext_of_ciccontext l)) | Cic.ASort (id,Cic.Prop) -> idref id (Ast.Sort `Prop) | Cic.ASort (id,Cic.Set) -> idref id (Ast.Sort `Set) - | Cic.ASort (id,Cic.Type) -> idref id (Ast.Sort `Type) + | Cic.ASort (id,Cic.Type _) -> idref id (Ast.Sort `Type) (* TASSI *) | Cic.ASort (id,Cic.CProp) -> idref id (Ast.Sort `CProp) | Cic.AImplicit _ -> assert false | Cic.AProd (id,n,s,t) -> diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml index ea7d1958d..b3467ad9e 100644 --- a/helm/ocaml/cic_transformations/cic2Xml.ml +++ b/helm/ocaml/cic_transformations/cic2Xml.ml @@ -74,7 +74,7 @@ let print_term ~ids_to_inner_sorts = function C.Prop -> "Prop" | C.Set -> "Set" - | C.Type -> "Type" + | C.Type _ -> "Type" (* TASSI *) | C.CProp -> "CProp" in X.xml_empty "SORT" [None,"value",(string_of_sort s) ; None,"id",id] diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml index 5fe5bc3dc..8c88fd01f 100644 --- a/helm/ocaml/cic_transformations/content_expressions.ml +++ b/helm/ocaml/cic_transformations/content_expressions.ml @@ -286,7 +286,7 @@ let string_of_sort = function Cic.Prop -> "Prop" | Cic.Set -> "Set" - | Cic.Type -> "Type" + | Cic.Type _ -> "Type" (* TASSI *) | Cic.CProp -> "Type" ;; diff --git a/helm/ocaml/cic_unification/cicMkImplicit.ml b/helm/ocaml/cic_unification/cicMkImplicit.ml index 0fa33047f..41f058945 100644 --- a/helm/ocaml/cic_unification/cicMkImplicit.ml +++ b/helm/ocaml/cic_unification/cicMkImplicit.ml @@ -51,32 +51,40 @@ let new_meta metasenv = let mk_implicit metasenv context = let newmeta = new_meta metasenv in + let newuniv = CicUniv.fresh () in let irl = identity_relocation_list_for_metavariable context in - ([ newmeta, [], Cic.Sort Cic.Type ; + ([ newmeta, [], Cic.Sort (Cic.Type newuniv) ; + (* TASSI: ?? *) newmeta + 1, context, Cic.Meta (newmeta, []); newmeta + 2, context, Cic.Meta (newmeta + 1,irl) ] @ metasenv, newmeta + 2) let mk_implicit_type metasenv context = let newmeta = new_meta metasenv in - ([ newmeta, [], Cic.Sort Cic.Type ; + let newuniv = CicUniv.fresh () in + ([ newmeta, [], Cic.Sort (Cic.Type newuniv); + (* TASSI: ?? *) newmeta + 1, context, Cic.Meta (newmeta, []) ] @metasenv, newmeta + 1) let mk_implicit_sort metasenv = let newmeta = new_meta metasenv in - ([ newmeta, [], Cic.Sort Cic.Type] @ metasenv, newmeta) + let newuniv = CicUniv.fresh () in + ([ newmeta, [], Cic.Sort (Cic.Type newuniv)] @ metasenv, newmeta) + (* TASSI: ?? *) let n_fresh_metas metasenv context n = if n = 0 then metasenv, [] else let irl = identity_relocation_list_for_metavariable context in let newmeta = new_meta metasenv in + let newuniv = CicUniv.fresh () in let rec aux newmeta n = if n = 0 then metasenv, [] else let metasenv', l = aux (newmeta + 3) (n-1) in - (newmeta, context, Cic.Sort Cic.Type):: + (* TASSI: ?? *) + (newmeta, context, Cic.Sort (Cic.Type newuniv)):: (newmeta + 1, context, Cic.Meta (newmeta, irl)):: (newmeta + 2, context, Cic.Meta (newmeta + 1,irl))::metasenv', Cic.Meta(newmeta+2,irl)::l in @@ -85,11 +93,13 @@ let n_fresh_metas metasenv context n = let fresh_subst metasenv context uris = let irl = identity_relocation_list_for_metavariable context in let newmeta = new_meta metasenv in + let newuniv = CicUniv.fresh () in let rec aux newmeta = function [] -> metasenv, [] | uri::tl -> let metasenv', l = aux (newmeta + 3) tl in - (newmeta, context, Cic.Sort Cic.Type):: + (* TASSI: ?? *) + (newmeta, context, Cic.Sort (Cic.Type newuniv)):: (newmeta + 1, context, Cic.Meta (newmeta, irl)):: (newmeta + 2, context, Cic.Meta (newmeta + 1,irl))::metasenv', (uri,Cic.Meta(newmeta+2,irl))::l in diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 14c69a457..b3525d318 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -161,9 +161,15 @@ and type_of_aux' metasenv context t = check_metasenv_consistency n subst metasenv context canonical_context l in CicSubstitution.lift_meta l ty, subst', metasenv' - | C.Sort s -> - C.Sort C.Type, (*CSC manca la gestione degli universi!!! *) - subst,metasenv + (* TASSI: CONSTRAINT *) + | C.Sort (C.Type t) -> + let t' = CicUniv.fresh() in + if not (CicUniv.add_gt t' t ) then + assert false (* t' is fresh! an error in CicUniv *) + else + C.Sort (C.Type t'),subst,metasenv + (* TASSI: CONSTRAINT *) + | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())),subst,metasenv | C.Implicit _ -> raise (AssertFailure "21") | C.Cast (te,ty) -> let _,subst',metasenv' = @@ -479,9 +485,15 @@ and type_of_aux' metasenv context t = (C.Sort s1, C.Sort s2) when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *) C.Sort s2,subst,metasenv - | (C.Sort s1, C.Sort s2) -> - (*CSC manca la gestione degli universi!!! *) - C.Sort C.Type,subst,metasenv + | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> + (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *) + let t' = CicUniv.fresh() in + if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then + assert false ; (* not possible, error in CicUniv *) + C.Sort (C.Type t'),subst,metasenv + | (C.Sort _,C.Sort (C.Type t1)) -> + (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *) + C.Sort (C.Type t1),subst,metasenv | (C.Meta _, C.Sort _) -> t2'',subst,metasenv | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) -> (* TODO how can we force the meta to become a sort? If we don't we diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index b9f87cf9a..35eb18f45 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -52,7 +52,7 @@ let type_of_aux' metasenv subst context term = a new substitution which is _NOT_ unwinded. It must be unwinded before applying it. *) -let rec fo_unif_subst subst context metasenv t1 t2 = +let rec fo_unif_subst test_equality_only subst context metasenv t1 t2 = let module C = Cic in let module R = CicMetaSubst in let module S = CicSubstitution in @@ -75,7 +75,8 @@ let rec fo_unif_subst subst context metasenv t1 t2 = else (try let subst,metasenv = - fo_unif_subst subst context metasenv t1' t2' + fo_unif_subst + test_equality_only subst context metasenv t1' t2' in true,subst,metasenv with @@ -93,7 +94,7 @@ let rec fo_unif_subst subst context metasenv t1 t2 = "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) | (C.Meta (n,_), C.Meta (m,_)) when n>m -> - fo_unif_subst subst context metasenv t2 t1 + fo_unif_subst test_equality_only subst context metasenv t2 t1 | (C.Meta (n,l), t) | (t, C.Meta (n,l)) -> let swap = @@ -104,14 +105,17 @@ let rec fo_unif_subst subst context metasenv t1 t2 = in let lower = fun x y -> if swap then y else x in let upper = fun x y -> if swap then x else y in - let fo_unif_subst_ordered subst context metasenv m1 m2 = - fo_unif_subst subst context metasenv (lower m1 m2) (upper m1 m2) + let fo_unif_subst_ordered + test_equality_only subst context metasenv m1 m2 = + fo_unif_subst test_equality_only subst context metasenv + (lower m1 m2) (upper m1 m2) in let subst'',metasenv' = try let oldt = (List.assoc n subst) in let lifted_oldt = S.lift_meta l oldt in - fo_unif_subst_ordered subst context metasenv t lifted_oldt + fo_unif_subst_ordered + test_equality_only subst context metasenv t lifted_oldt with Not_found -> let t',metasenv',subst' = try @@ -120,14 +124,25 @@ let rec fo_unif_subst subst context metasenv t1 t2 = (CicMetaSubst.MetaSubstFailure msg)-> raise(UnificationFailure msg) | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg) in - (n, t')::subst', metasenv' + let t'' = + match t' with + C.Sort (C.Type u) when not test_equality_only -> + let u' = CicUniv.fresh () in + let s = C.Sort (C.Type u') in + ignore (CicUniv.add_ge (upper u u') (lower u u')) ; + s + | _ -> t' + in + (n, t'')::subst', metasenv' in let (_,_,meta_type) = CicUtil.lookup_meta n metasenv' in (try let tyt = type_of_aux' metasenv' subst'' context t in - fo_unif_subst subst'' context metasenv' tyt (S.lift_meta l meta_type) + fo_unif_subst + test_equality_only + subst'' context metasenv' tyt (S.lift_meta l meta_type) with AssertFailure _ -> (* TODO huge hack!!!! * we keep on unifying/refining in the hope that the problem will be @@ -143,7 +158,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2)) | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) -> if UriManager.eq uri1 uri2 then - fo_unif_subst_exp_named_subst subst context metasenv + fo_unif_subst_exp_named_subst test_equality_only subst context metasenv exp_named_subst1 exp_named_subst2 else raise (UnificationFailure (sprintf @@ -151,7 +166,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) -> if UriManager.eq uri1 uri2 && i1 = i2 then - fo_unif_subst_exp_named_subst subst context metasenv + fo_unif_subst_exp_named_subst test_equality_only subst context metasenv exp_named_subst1 exp_named_subst2 else raise (UnificationFailure (sprintf @@ -160,52 +175,62 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; | C.MutConstruct (uri1,i1,j1,exp_named_subst1), C.MutConstruct (uri2,i2,j2,exp_named_subst2) -> if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then - fo_unif_subst_exp_named_subst subst context metasenv + fo_unif_subst_exp_named_subst test_equality_only subst context metasenv exp_named_subst1 exp_named_subst2 else raise (UnificationFailure (sprintf "Can't unify %s with %s due to different inductive constructors" (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) | (C.Implicit _, _) | (_, C.Implicit _) -> assert false - | (C.Cast (te,ty), t2) -> fo_unif_subst subst context metasenv te t2 - | (t1, C.Cast (te,ty)) -> fo_unif_subst subst context metasenv t1 te + | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only + subst context metasenv te t2 + | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only + subst context metasenv t1 te | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> - let subst',metasenv' = fo_unif_subst subst context metasenv s1 s2 in - fo_unif_subst subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 + (* TASSI: this is the only case in which we want == *) + let subst',metasenv' = fo_unif_subst true + subst context metasenv s1 s2 in + fo_unif_subst test_equality_only + subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) -> - let subst',metasenv' = fo_unif_subst subst context metasenv s1 s2 in - fo_unif_subst subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 + (* TASSI: ask someone a reason for not putting true here *) + let subst',metasenv' = fo_unif_subst test_equality_only + subst context metasenv s1 s2 in + fo_unif_subst test_equality_only + subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 | (C.LetIn (_,s1,t1), t2) | (t2, C.LetIn (_,s1,t1)) -> - fo_unif_subst subst context metasenv t2 (S.subst s1 t1) + fo_unif_subst + test_equality_only subst context metasenv t2 (S.subst s1 t1) | (C.Appl l1, C.Appl l2) -> let lr1 = List.rev l1 in let lr2 = List.rev l2 in - let rec fo_unif_l subst metasenv = + let rec fo_unif_l test_equality_only subst metasenv = function [],_ | _,[] -> assert false | ([h1],[h2]) -> - fo_unif_subst subst context metasenv h1 h2 + fo_unif_subst test_equality_only subst context metasenv h1 h2 | ([h],l) | (l,[h]) -> - fo_unif_subst subst context metasenv h (C.Appl (List.rev l)) + fo_unif_subst + test_equality_only subst context metasenv h (C.Appl (List.rev l)) | ((h1::l1),(h2::l2)) -> let subst', metasenv' = - fo_unif_subst subst context metasenv h1 h2 + fo_unif_subst test_equality_only subst context metasenv h1 h2 in - fo_unif_l subst' metasenv' (l1,l2) + fo_unif_l test_equality_only subst' metasenv' (l1,l2) in - fo_unif_l subst metasenv (lr1, lr2) + fo_unif_l test_equality_only subst metasenv (lr1, lr2) | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))-> let subst', metasenv' = - fo_unif_subst subst context metasenv outt1 outt2 in + fo_unif_subst test_equality_only subst context metasenv outt1 outt2 in let subst'',metasenv'' = - fo_unif_subst subst' context metasenv' t1' t2' in + fo_unif_subst test_equality_only subst' context metasenv' t1' t2' in (try List.fold_left2 (function (subst,metasenv) -> - fo_unif_subst subst context metasenv + fo_unif_subst test_equality_only subst context metasenv ) (subst'',metasenv'') pl1 pl2 with Invalid_argument _ -> @@ -232,14 +257,14 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; "Can't unify %s with %s because they are not convertible" (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) -and fo_unif_subst_exp_named_subst subst context metasenv +and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv exp_named_subst1 exp_named_subst2 = try List.fold_left2 (fun (subst,metasenv) (uri1,t1) (uri2,t2) -> assert (uri1=uri2) ; - fo_unif_subst subst context metasenv t1 t2 + fo_unif_subst test_equality_only subst context metasenv t1 t2 ) (subst,metasenv) exp_named_subst1 exp_named_subst2 with Invalid_argument _ -> @@ -260,7 +285,8 @@ and fo_unif_subst_exp_named_subst subst context metasenv (* a new substitution which is already unwinded and ready to be applied and *) (* a new metasenv in which some hypothesis in the contexts of the *) (* metavariables may have been restricted. *) -let fo_unif metasenv context t1 t2 = fo_unif_subst [] context metasenv t1 t2 ;; +let fo_unif metasenv context t1 t2 = + fo_unif_subst false [] context metasenv t1 t2 ;; let fo_unif_subst subst context metasenv t1 t2 = let enrich_msg msg = @@ -277,7 +303,7 @@ let fo_unif_subst subst context metasenv t1 t2 = (CicMetaSubst.ppmetasenv metasenv subst) msg in try - fo_unif_subst subst context metasenv t1 t2 + fo_unif_subst false subst context metasenv t1 t2 with | AssertFailure msg -> raise (AssertFailure (enrich_msg msg)) | UnificationFailure msg -> raise (UnificationFailure (enrich_msg msg)) diff --git a/helm/ocaml/getter/.depend b/helm/ocaml/getter/.depend index 59d5b4c8e..295c638b9 100644 --- a/helm/ocaml/getter/.depend +++ b/helm/ocaml/getter/.depend @@ -6,14 +6,14 @@ clientHTTP.cmo: clientHTTP.cmi clientHTTP.cmx: clientHTTP.cmi http_getter_logger.cmo: http_getter_logger.cmi http_getter_logger.cmx: http_getter_logger.cmi -http_getter_misc.cmo: http_getter_misc.cmi -http_getter_misc.cmx: http_getter_misc.cmi +http_getter_misc.cmo: http_getter_logger.cmi http_getter_misc.cmi +http_getter_misc.cmx: http_getter_logger.cmx http_getter_misc.cmi http_getter_const.cmo: http_getter_const.cmi http_getter_const.cmx: http_getter_const.cmi -http_getter_env.cmo: http_getter_const.cmi http_getter_misc.cmi \ - http_getter_types.cmo http_getter_env.cmi -http_getter_env.cmx: http_getter_const.cmx http_getter_misc.cmx \ - http_getter_types.cmx http_getter_env.cmi +http_getter_env.cmo: http_getter_const.cmi http_getter_logger.cmi \ + http_getter_misc.cmi http_getter_types.cmo http_getter_env.cmi +http_getter_env.cmx: http_getter_const.cmx http_getter_logger.cmx \ + http_getter_misc.cmx http_getter_types.cmx http_getter_env.cmi http_getter_common.cmo: http_getter_env.cmi http_getter_misc.cmi \ http_getter_types.cmo http_getter_common.cmi http_getter_common.cmx: http_getter_env.cmx http_getter_misc.cmx \ @@ -21,12 +21,16 @@ http_getter_common.cmx: http_getter_env.cmx http_getter_misc.cmx \ http_getter_map.cmo: http_getter_map.cmi http_getter_map.cmx: http_getter_map.cmi http_getter_cache.cmo: http_getter_common.cmi http_getter_env.cmi \ - http_getter_misc.cmi http_getter_types.cmo http_getter_cache.cmi + http_getter_logger.cmi http_getter_misc.cmi http_getter_types.cmo \ + http_getter_cache.cmi http_getter_cache.cmx: http_getter_common.cmx http_getter_env.cmx \ - http_getter_misc.cmx http_getter_types.cmx http_getter_cache.cmi + http_getter_logger.cmx http_getter_misc.cmx http_getter_types.cmx \ + http_getter_cache.cmi http_getter.cmo: clientHTTP.cmi http_getter_cache.cmi http_getter_common.cmi \ - http_getter_const.cmi http_getter_env.cmi http_getter_map.cmi \ - http_getter_misc.cmi http_getter_types.cmo http_getter.cmi + http_getter_const.cmi http_getter_env.cmi http_getter_logger.cmi \ + http_getter_map.cmi http_getter_misc.cmi http_getter_types.cmo \ + http_getter.cmi http_getter.cmx: clientHTTP.cmx http_getter_cache.cmx http_getter_common.cmx \ - http_getter_const.cmx http_getter_env.cmx http_getter_map.cmx \ - http_getter_misc.cmx http_getter_types.cmx http_getter.cmi + http_getter_const.cmx http_getter_env.cmx http_getter_logger.cmx \ + http_getter_map.cmx http_getter_misc.cmx http_getter_types.cmx \ + http_getter.cmi diff --git a/helm/ocaml/mathql_generator/cGSearchPattern.ml b/helm/ocaml/mathql_generator/cGSearchPattern.ml index 559bee6d9..b0d290578 100644 --- a/helm/ocaml/mathql_generator/cGSearchPattern.ml +++ b/helm/ocaml/mathql_generator/cGSearchPattern.ml @@ -95,7 +95,7 @@ let get_constraints term = match s with Cic.Prop -> T.Prop | Cic.Set -> T.Set - | Cic.Type -> T.Type + | Cic.Type _ -> T.Type (* TASSI: ?? *) | Cic.CProp -> T.CProp in [],[],[!!kind,s'] diff --git a/helm/ocaml/mathql_interpreter/.depend b/helm/ocaml/mathql_interpreter/.depend index c675ba352..f7a04516b 100644 --- a/helm/ocaml/mathql_interpreter/.depend +++ b/helm/ocaml/mathql_interpreter/.depend @@ -1,7 +1,7 @@ mQIPostgres.cmi: mQITypes.cmo mQIMySql.cmi: mQITypes.cmo mQIConn.cmi: mQIMap.cmi mQITypes.cmo -mQIProperty.cmi: mQIConn.cmi +mQIProperty.cmi: mQIConn.cmi mQITypes.cmo mQueryInterpreter.cmi: mQIConn.cmi mQueryTParser.cmo: mQueryTParser.cmi mQueryTParser.cmx: mQueryTParser.cmi diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend index 683e59f88..608260c83 100644 --- a/helm/ocaml/tactics/.depend +++ b/helm/ocaml/tactics/.depend @@ -16,8 +16,6 @@ proofEngineReduction.cmo: proofEngineReduction.cmi proofEngineReduction.cmx: proofEngineReduction.cmi proofEngineHelpers.cmo: proofEngineHelpers.cmi proofEngineHelpers.cmx: proofEngineHelpers.cmi -fourier.cmo: fourier.cmi -fourier.cmx: fourier.cmi tacticals.cmo: proofEngineTypes.cmo tacticals.cmi tacticals.cmx: proofEngineTypes.cmx tacticals.cmi reductionTactics.cmo: proofEngineReduction.cmi reductionTactics.cmi @@ -70,6 +68,8 @@ ring.cmo: eliminationTactics.cmi equalityTactics.cmi primitiveTactics.cmi \ ring.cmx: eliminationTactics.cmx equalityTactics.cmx primitiveTactics.cmx \ proofEngineStructuralRules.cmx proofEngineTypes.cmx tacticals.cmx \ ring.cmi +fourier.cmo: fourier.cmi +fourier.cmx: fourier.cmi fourierR.cmo: equalityTactics.cmi fourier.cmi primitiveTactics.cmi \ proofEngineHelpers.cmi proofEngineTypes.cmo reductionTactics.cmi ring.cmi \ tacticals.cmi fourierR.cmi diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index 812094d5a..388ac2056 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -160,12 +160,13 @@ let new_metasenv_for_apply newmeta proof context ty = let rec aux newmeta = function C.Cast (he,_) -> aux newmeta he -(* CSC: patch to generate ?1 : ?2 : Type in place of ?1 : Type +(* CSC: patch to generate ?1 : ?2 : Type in place of ?1 : Type to simulate ?1 :< Type (* If the expected type is a Type, then also Set is OK ==> * we accept any term of type Type *) (*CSC: BUG HERE: in this way it is possible for the term of * type Type to be different from a Sort!!! *) - | C.Prod (name,(C.Sort C.Type as s),t) -> + | C.Prod (name,(C.Sort (C.Type _) as s),t) -> + (* TASSI: ask CSC if BUG HERE refers to the C.Cast or C.Propd case *) let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in @@ -219,15 +220,16 @@ let CicSubstitution.subst_vars !exp_named_subst_diff ty | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri)) in -(* CSC: patch to generate ?1 : ?2 : Type in place of ?1 : Type +(* CSC: patch to generate ?1 : ?2 : Type in place of ?1 : Type to simulate ?1 :< Type (match ty with - C.Sort C.Type as s -> + C.Sort (C.Type _) as s -> (* TASSI: ?? *) let fresh_meta = !next_fresh_meta in let fresh_meta' = fresh_meta + 1 in next_fresh_meta := !next_fresh_meta + 2 ; let subst_item = uri,C.Meta (fresh_meta',[]) in newmetasenvfragment := - (fresh_meta,[],C.Sort C.Type) :: + (fresh_meta,[],C.Sort (C.Type (CicUniv.fresh()))) :: + (* TASSI: ?? *) (fresh_meta',[],C.Meta (fresh_meta,[])) :: !newmetasenvfragment ; exp_named_subst_diff := !exp_named_subst_diff @ [subst_item] ; subst_item::(aux (tl,[])) @@ -461,7 +463,7 @@ let elim_tac ~term (proof, goal) = C.Sort C.Prop -> "_ind" | C.Sort C.Set -> "_rec" | C.Sort C.CProp -> "_rec" - | C.Sort C.Type -> "_rect" + | C.Sort (C.Type _)-> "_rect" (* TASSI *) | _ -> assert false in U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly index 3ca69d5c6..41a36acc6 100644 --- a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly +++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly @@ -136,12 +136,14 @@ let mk_implicit () = let newmeta = new_meta () in + let newuniv = CicUniv.fresh () in let new_canonical_context = [] in let irl = identity_relocation_list_for_metavariable new_canonical_context in TexCicTextualParser0.metasenv := - [newmeta, new_canonical_context, Sort Type ; + [newmeta, new_canonical_context, Sort (Type newuniv); + (* TASSI: ?? *) newmeta+1, new_canonical_context, Meta (newmeta,irl); newmeta+2, new_canonical_context, Meta (newmeta+1,irl) ] @ !TexCicTextualParser0.metasenv ; @@ -422,7 +424,7 @@ expr2: { mk_implicit () } | SET { [], function _ -> Sort Set } | PROP { [], function _ -> Sort Prop } - | TYPE { [], function _ -> Sort Type } + | TYPE { [], function _ -> Sort (Type (CicUniv.fresh ())) (* TASSI: ?? *)} | CPROP { [], function _ -> Sort CProp } | LPAREN expr CAST expr RPAREN { let dom1,mk_expr1 = $2 in @@ -562,12 +564,14 @@ pihead: { TexCicTextualParser0.binders := (Some (Name $2))::!TexCicTextualParser0.binders; let newmeta = new_meta () in + let newuniv = CicUniv.fresh () in let new_canonical_context = [] in let irl = identity_relocation_list_for_metavariable new_canonical_context in TexCicTextualParser0.metasenv := - [newmeta, new_canonical_context, Sort Type ; + [newmeta, new_canonical_context, Sort (Type newuniv); + (* TASSI: ?? *) newmeta+1, new_canonical_context, Meta (newmeta,irl) ] @ !TexCicTextualParser0.metasenv ; Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl)) @@ -584,12 +588,14 @@ lambdahead: { TexCicTextualParser0.binders := (Some (Name $2))::!TexCicTextualParser0.binders; let newmeta = new_meta () in + let newuniv = CicUniv.fresh () in let new_canonical_context = [] in let irl = identity_relocation_list_for_metavariable new_canonical_context in TexCicTextualParser0.metasenv := - [newmeta, new_canonical_context, Sort Type ; + [newmeta, new_canonical_context, Sort (Type newuniv) ; + (* TASSI: ?? *) newmeta+1, new_canonical_context, Meta (newmeta,irl) ] @ !TexCicTextualParser0.metasenv ; Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl)) -- 2.39.2