From 37f08b2aba9f17d9d609ca0f57d607f437a3d3fc Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 20 May 2002 08:39:06 +0000 Subject: [PATCH] New experimental commit: metavariables representation is changed again, together with the DTD (still uncommitted). The new representation implements explicit substitutions, allowing the correct reduction behaviour. The most part of the modules have been changed to reflect the new representation. Unification has been rewritten. --- helm/ocaml/cic/cic.ml | 27 +- helm/ocaml/cic/cicParser.ml | 5 +- helm/ocaml/cic/cicParser2.ml | 36 +- helm/ocaml/cic/cicParser3.ml | 15 +- helm/ocaml/cic/deannotate.ml | 25 +- .../cic_annotations/cicAnnotation2Xml.ml | 22 +- helm/ocaml/cic_annotations/cicXPath.ml | 13 +- helm/ocaml/cic_proof_checking/.cvsignore | 1 + helm/ocaml/cic_proof_checking/.depend | 4 +- helm/ocaml/cic_proof_checking/cicPp.ml | 53 +- helm/ocaml/cic_proof_checking/cicPp.mli | 2 +- .../cic_proof_checking/cicReductionMachine.ml | 6 +- .../cic_proof_checking/cicReductionNaif.ml | 21 +- .../cic_proof_checking/cicSubstitution.ml | 188 +++++- .../cic_proof_checking/cicSubstitution.mli | 3 + .../cic_proof_checking/cicTypeChecker.ml | 284 +++++---- .../cic_proof_checking/cicTypeChecker.mli | 2 +- .../cic_textual_parser/cicTextualLexer.mll | 3 + .../cic_textual_parser/cicTextualParser.mly | 30 +- .../cic_textual_parser/cicTextualParser0.ml | 2 +- .../cicTextualParserContext.mli | 2 +- helm/ocaml/cic_unification/cicUnification.ml | 562 +++++++++++------- helm/ocaml/cic_unification/cicUnification.mli | 3 +- 23 files changed, 932 insertions(+), 377 deletions(-) diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml index 0a43c4c57..550d4a8f6 100644 --- a/helm/ocaml/cic/cic.ml +++ b/helm/ocaml/cic/cic.ml @@ -52,7 +52,8 @@ and name = and term = Rel of int (* DeBrujin index *) | Var of UriManager.uri (* uri *) - | Meta of int (* numeric id *) + | Meta of int * (term option) list (* numeric id, *) + (* local context *) | Sort of sort (* sort *) | Implicit (* *) | Cast of term * term (* value, type *) @@ -78,7 +79,7 @@ and obj = | Axiom of string * term * (int * UriManager.uri list) list (* id, type, parameters *) | Variable of string * term option * term (* name, body, type *) - | CurrentProof of string * (int * term) list * (* name, conjectures, *) + | CurrentProof of string * metasenv * (* name, conjectures, *) term * term (* value, type *) | InductiveDefinition of inductiveType list * (* inductive types, *) (int * UriManager.uri list) list * int (* parameters, n ind. pars *) @@ -92,10 +93,15 @@ and inductiveFun = and coInductiveFun = string * term * term (* name, type, body *) +and metasenv = (int * context * term) list (* a metasenv is a list of declarations of metas *) + +and annmetasenv = (int * anncontext * annterm) list (* a metasenv is a list of declarations of metas *) + and annterm = ARel of id * int * string (* DeBrujin index, binder *) | AVar of id * UriManager.uri (* uri *) - | AMeta of id * int (* numeric id *) + | AMeta of id * int * (annterm option) list (* numeric id, *) + (* local context *) | ASort of id * sort (* sort *) | AImplicit of id (* *) | ACast of id * annterm * annterm (* value, type *) @@ -124,7 +130,7 @@ and annobj = | AVariable of id * string * annterm option * annterm (* name, body, type *) | ACurrentProof of id * - string * (int * annterm) list * (* name, conjectures, *) + string * annmetasenv * (* name, conjectures, *) annterm * annterm (* value, type *) | AInductiveDefinition of id * anninductiveType list * (* inductive types , *) @@ -143,12 +149,15 @@ and annotation = and 'a exactness = Possible of 'a (* an approximation to something *) | Actual of 'a (* something *) -;; -(* Contexts are lists of context_entry *) -type context_entry = +and context_entry = (* Contexts are lists of context_entry *) Decl of term | Def of term -;; -type context = context_entry list;; +and context = ((name * context_entry) option) list + +and anncontext_entry = (* Contexts are lists of context_entry *) + ADecl of annterm + | ADef of annterm + +and anncontext = ((name * anncontext_entry) option) list;; diff --git a/helm/ocaml/cic/cicParser.ml b/helm/ocaml/cic/cicParser.ml index f0d3e800f..241a5c175 100644 --- a/helm/ocaml/cic/cicParser.ml +++ b/helm/ocaml/cic/cicParser.ml @@ -46,7 +46,7 @@ class warner = end ;; -exception EmptyUri;; +exception EmptyUri of string;; (* given an uri u it returns the list of tokens of the base uri of u *) (* e.g.: token_of_uri "cic:/a/b/c/d.xml" returns ["a" ; "b" ; "c"] *) @@ -54,7 +54,8 @@ let tokens_of_uri uri = let uri' = UriManager.string_of_uri uri in let rec chop_list = function - [] -> raise EmptyUri + [] -> raise (EmptyUri uri') + | [fn] -> [] | he::[fn] -> [he] | he::tl -> he::(chop_list tl) in diff --git a/helm/ocaml/cic/cicParser2.ml b/helm/ocaml/cic/cicParser2.ml index 0dbf9f410..4865c6e4a 100644 --- a/helm/ocaml/cic/cicParser2.ml +++ b/helm/ocaml/cic/cicParser2.ml @@ -118,6 +118,15 @@ let bool_of_attr a = bool_of_string (string_of_attr a) ;; +let name_of_attr a = + let module T = Pxp_types in + let module C = Cic in + match a with + T.Value s -> C.Name s + | T.Implied_value -> C.Anonimous + | _ -> raise (IllFormedXml 0) +;; + (* Other utility functions *) let get_content n = @@ -142,9 +151,28 @@ let get_conjs_value_type l = match l with [] -> (c, v, t) | conj::tl when conj#node_type = D.T_element "Conjecture" -> - let no = int_of_attr (conj#attribute "no") - and typ = (get_content conj)#extension#to_cic_term in - rget ((no, typ)::c, v, t) tl + let no = int_of_attr (conj#attribute "no") in + let typ,canonical_context = + match List.rev (conj#sub_nodes) with + [] -> raise (IllFormedXml 13) + | typ::canonical_context -> + (get_content typ)#extension#to_cic_term, + List.map + (function n -> + match n#node_type with + D.T_element "Decl" -> + let name = name_of_attr (n#attribute "name") in + let term = (get_content n)#extension#to_cic_term in + Some (name,Cic.ADecl term) + | D.T_element "Def" -> + let name = name_of_attr (n#attribute "name") in + let term = (get_content n)#extension#to_cic_term in + Some (name,Cic.ADef term) + | D.T_element "Hidden" -> None + | _ -> raise (IllFormedXml 14) + ) canonical_context + in + rget ((no, canonical_context, typ)::c, v, t) tl | value::tl when value#node_type = D.T_element "body" -> let v' = (get_content value)#extension#to_cic_term in (match v with @@ -160,7 +188,7 @@ let get_conjs_value_type l = | _ -> raise (IllFormedXml 4) in match rget ([], None, None) l with - (c, Some v, Some t) -> (c, v, t) + (revc, Some v, Some t) -> (List.rev revc, v, t) | _ -> raise (IllFormedXml 5) ;; diff --git a/helm/ocaml/cic/cicParser3.ml b/helm/ocaml/cic/cicParser3.ml index 82ca49692..72882a186 100644 --- a/helm/ocaml/cic/cicParser3.ml +++ b/helm/ocaml/cic/cicParser3.ml @@ -231,8 +231,19 @@ class eltype_meta = method to_cic_term = let n = self#node in let value = int_of_xml_attr (n#attribute "no") - and id = string_of_xml_attr (n#attribute "id") in - Cic.AMeta (id,value) + and id = string_of_xml_attr (n#attribute "id") + in + let local_context = + let sons = n#sub_nodes in + List.map + (function substitution -> + match substitution#sub_nodes with + [] -> None + | [he] -> Some he#extension#to_cic_term + | _ -> raise (IllFormedXml 20) + ) sons + in + Cic.AMeta (id,value,local_context) end ;; diff --git a/helm/ocaml/cic/deannotate.ml b/helm/ocaml/cic/deannotate.ml index 2445c3771..f0ae11879 100644 --- a/helm/ocaml/cic/deannotate.ml +++ b/helm/ocaml/cic/deannotate.ml @@ -27,12 +27,21 @@ let expect_possible_parameters = ref false;; exception NotExpectingPossibleParameters;; +(* converts annotated terms into cic terms (forgetting ids and names) *) let rec deannotate_term = let module C = Cic in function C.ARel (_,n,_) -> C.Rel n | C.AVar (_,uri) -> C.Var uri - | C.AMeta (_,n) -> C.Meta n + | C.AMeta (_,n, l) -> + let l' = + List.map + (function + None -> None + | Some at -> Some (deannotate_term at) + ) l + in + C.Meta (n, l') | C.ASort (_,s) -> C.Sort s | C.AImplicit _ -> C.Implicit | C.ACast (_,va,ty) -> C.Cast (deannotate_term va, deannotate_term ty) @@ -89,7 +98,19 @@ let deannotate_obj = deannotate_term ty) | C.ACurrentProof (_, name, conjs, bo, ty) -> C.CurrentProof ( - name, List.map (fun (id,con) -> (id,deannotate_term con)) conjs, + name, + List.map + (function + (id,acontext,con) -> + let context = + List.map + (function + Some (n,(C.ADef at)) -> Some (n,(C.Def (deannotate_term at))) + | Some (n,(C.ADecl at)) ->Some (n,(C.Decl (deannotate_term at))) + | None -> None) acontext + in + (id,context, deannotate_term con) + ) conjs, deannotate_term bo, deannotate_term ty ) | C.AInductiveDefinition (_, tys, params, parno) -> diff --git a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml index 8d12434cb..8fb002f3f 100644 --- a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml +++ b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml @@ -42,6 +42,8 @@ let print_ann i2a id = ;; (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *) +(* It takes in input a hash table mapping ids to annotations, an annotated +term, and gives back a Xml.token Stream.t representing the .ann file *) let print_term i2a = let rec aux = let module C = Cic in @@ -50,7 +52,7 @@ let print_term i2a = function C.ARel (id,_,_) -> print_ann i2a id | C.AVar (id,_) -> print_ann i2a id - | C.AMeta (id,_) -> print_ann i2a id + | C.AMeta (id,_,_) -> print_ann i2a id | C.ASort (id,_) -> print_ann i2a id | C.AImplicit _ -> raise NotImplemented | C.AProd (id,_,s,t) -> [< print_ann i2a id ; aux s ; aux t >] @@ -117,8 +119,19 @@ let pp_annotation obj i2a curi = | C.ACurrentProof (xid, _, conjs, bo, ty) -> [< print_ann i2a xid ; List.fold_right - (fun (_,t) i -> [< print_term i2a t ; i >]) - conjs [<>] ; + (fun (_, context, t) i -> + [< List.fold_right + (fun context_entry i -> + [<(match context_entry with + Some (_,C.ADecl at) -> print_term i2a at + | Some (_,C.ADef at) -> print_term i2a at + | None -> [< >] + ) ; i + >] + ) context [< >]; + print_term i2a t ; i + >] + ) conjs [<>] ; print_term i2a bo ; print_term i2a ty >] @@ -131,3 +144,6 @@ let pp_annotation obj i2a curi = end >] ;; + + + diff --git a/helm/ocaml/cic_annotations/cicXPath.ml b/helm/ocaml/cic_annotations/cicXPath.ml index 1eaf31f4e..76cb7f75a 100644 --- a/helm/ocaml/cic_annotations/cicXPath.ml +++ b/helm/ocaml/cic_annotations/cicXPath.ml @@ -42,6 +42,8 @@ let get_annotation ids_to_annotations xpath = exception MoreThanOneTargetFor of Cic.id;; +(* creates a hashtable mapping each unique id to a node of the annotated +object *) let get_ids_to_targets annobj = let module C = Cic in let ids_to_targets = Hashtbl.create 503 in @@ -56,7 +58,7 @@ let get_ids_to_targets annobj = match t with C.ARel (id,_,_) | C.AVar (id,_) - | C.AMeta (id,_) + | C.AMeta (id,_,_) | C.ASort (id,_) | C.AImplicit id -> set_target id (C.Term t) @@ -114,7 +116,14 @@ let get_ids_to_targets annobj = add_target_term ty | C.ACurrentProof (id,_,cl,bo,ty) -> set_target id (C.Object annobj) ; - List.iter (function (_,t) -> add_target_term t) cl ; + List.iter (function (_,context, t) -> + List.iter + (function + Some (_,C.ADecl at) -> add_target_term at + | Some (_,C.ADef at) -> add_target_term at + | None -> () + ) context; + add_target_term t) cl ; add_target_term bo ; add_target_term ty | C.AInductiveDefinition (id,itl,_,_) -> diff --git a/helm/ocaml/cic_proof_checking/.cvsignore b/helm/ocaml/cic_proof_checking/.cvsignore index 6b3eba302..1e0e8c7f0 100644 --- a/helm/ocaml/cic_proof_checking/.cvsignore +++ b/helm/ocaml/cic_proof_checking/.cvsignore @@ -1 +1,2 @@ *.cm[iaox] *.cmxa +cicReduction.ml diff --git a/helm/ocaml/cic_proof_checking/.depend b/helm/ocaml/cic_proof_checking/.depend index e03d3e436..04373b39e 100644 --- a/helm/ocaml/cic_proof_checking/.depend +++ b/helm/ocaml/cic_proof_checking/.depend @@ -13,8 +13,8 @@ cicReduction.cmo: cicEnvironment.cmi cicPp.cmi cicSubstitution.cmi \ cicReduction.cmx: cicEnvironment.cmx cicPp.cmx cicSubstitution.cmx \ cicReduction.cmi cicTypeChecker.cmo: cicEnvironment.cmi cicPp.cmi cicReduction.cmi \ - cicSubstitution.cmi cicTypeChecker.cmi + cicSubstitution.cmi logger.cmi cicTypeChecker.cmi cicTypeChecker.cmx: cicEnvironment.cmx cicPp.cmx cicReduction.cmx \ - cicSubstitution.cmx cicTypeChecker.cmi + cicSubstitution.cmx logger.cmx cicTypeChecker.cmi cicCooking.cmo: cicEnvironment.cmi cicCooking.cmi cicCooking.cmx: cicEnvironment.cmx cicCooking.cmi diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml index 745a203a4..07e306b0b 100644 --- a/helm/ocaml/cic_proof_checking/cicPp.ml +++ b/helm/ocaml/cic_proof_checking/cicPp.ml @@ -67,14 +67,18 @@ let rec pp t l = begin try (match get_nth l n with - C.Name s -> s + Some (C.Name s) -> s | _ -> raise CicPpInternalError ) with NotEnoughElements -> string_of_int (List.length l - n) end | C.Var uri -> UriManager.name_of_uri uri - | C.Meta n -> "?" ^ (string_of_int n) + | C.Meta (n,l1) -> + "?" ^ (string_of_int n) ^ "[" ^ + String.concat " ; " + (List.map (function None -> "_" | Some t -> pp t l) l1) ^ + "]" | C.Sort s -> (match s with C.Prop -> "Prop" @@ -84,14 +88,14 @@ let rec pp t l = | C.Implicit -> "?" | C.Prod (b,s,t) -> (match b with - C.Name n -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t (b::l) - | C.Anonimous -> "(" ^ pp s l ^ "->" ^ pp t (b::l) ^ ")" + C.Name n -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t ((Some b)::l) + | C.Anonimous -> "(" ^ pp s l ^ "->" ^ pp t ((Some b)::l) ^ ")" ) | C.Cast (v,t) -> pp v l | C.Lambda (b,s,t) -> - "[" ^ string_of_name b ^ ":" ^ pp s l ^ "]" ^ pp t (b::l) + "[" ^ string_of_name b ^ ":" ^ pp s l ^ "]" ^ pp t ((Some b)::l) | C.LetIn (b,s,t) -> - "[" ^ string_of_name b ^ ":=" ^ pp s l ^ "]" ^ pp t (b::l) + "[" ^ string_of_name b ^ ":=" ^ pp s l ^ "]" ^ pp t ((Some b)::l) | C.Appl li -> "(" ^ (List.fold_right @@ -130,7 +134,9 @@ let rec pp t l = "\nend" | C.Fix (no, funs) -> let snames = List.map (fun (name,_,_,_) -> name) funs in - let names = List.rev (List.map (function name -> C.Name name) snames) in + let names = + List.rev (List.map (function name -> Some (C.Name name)) snames) + in "\nFix " ^ get_nth snames (no + 1) ^ " {" ^ List.fold_right (fun (name,ind,ty,bo) i -> "\n" ^ name ^ " / " ^ string_of_int ind ^ @@ -140,7 +146,9 @@ let rec pp t l = "}\n" | C.CoFix (no,funs) -> let snames = List.map (fun (name,_,_) -> name) funs in - let names = List.rev (List.map (function name -> C.Name name) snames) in + let names = + List.rev (List.map (function name -> Some (C.Name name)) snames) + in "\nCoFix " ^ get_nth snames (no + 1) ^ " {" ^ List.fold_right (fun (name,ty,bo) i -> "\n" ^ name ^ @@ -202,10 +210,29 @@ let ppobj obj = (match bo with None -> "" | Some bo -> ":= " ^ pp bo []) | C.CurrentProof (name, conjectures, value, ty) -> "Current Proof:\n" ^ - List.fold_right - (fun (n, t) i -> "?" ^ (string_of_int n) ^ ": " ^ pp t [] ^ "\n" ^ i) - conjectures "" ^ - "\n" ^ pp value [] ^ " : " ^ pp ty [] + let separate s = if s = "" then "" else s ^ " ; " in + List.fold_right + (fun (n, context, t) i -> + let conjectures',name_context = + List.fold_right + (fun context_entry (i,name_context) -> + (match context_entry with + Some (n,C.Decl at) -> + (separate i) ^ + string_of_name n ^ ":" ^ pp at name_context ^ " ", + (Some n)::name_context + | Some (n,C.Def at) -> + (separate i) ^ + string_of_name n ^ ":= " ^ pp at name_context ^ " ", + (Some n)::name_context + | None -> + (separate i) ^ "_ :? _ ", None::name_context) + ) context ("",[]) + in + conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^ + pp t name_context ^ "\n" ^ i + ) conjectures "" ^ + "\n" ^ pp value [] ^ " : " ^ pp ty [] | C.InductiveDefinition (l, params, nparams) -> "Parameters = " ^ List.fold_right @@ -216,6 +243,6 @@ let ppobj obj = ) x "" ^ match i with "" -> "" | i' -> " " ^ i' ) params "" ^ "\n" ^ "NParams = " ^ string_of_int nparams ^ "\n" ^ - let names = List.rev (List.map (fun (n,_,_,_) -> C.Name n) l) in + let names = List.rev (List.map (fun (n,_,_,_) -> Some (C.Name n)) l) in List.fold_right (fun x i -> ppinductiveType x names ^ i) l "" ;; diff --git a/helm/ocaml/cic_proof_checking/cicPp.mli b/helm/ocaml/cic_proof_checking/cicPp.mli index afc519c9f..9f68d0525 100644 --- a/helm/ocaml/cic_proof_checking/cicPp.mli +++ b/helm/ocaml/cic_proof_checking/cicPp.mli @@ -44,4 +44,4 @@ val ppterm : Cic.term -> string (* Required only by the topLevel. It is the generalization of ppterm to *) (* work with environments. *) -val pp : Cic.term -> Cic.name list -> string +val pp : Cic.term -> (Cic.name option) list -> string diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml index c69ef5b75..d0e103521 100644 --- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml +++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml @@ -66,7 +66,7 @@ let unwind' m k e t = else S.lift m t' | None -> C.Rel (n-k)) | C.Var _ as t -> t - | C.Meta _ as t -> t + | C.Meta (i,l) as t -> t | C.Sort _ as t -> t | C.Implicit as t -> t | C.Cast (te,ty) -> C.Cast (unwind_aux m te, unwind_aux m ty) (*CSC ??? *) @@ -380,3 +380,7 @@ in + + + + diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml index 1ab5e92bc..089906b6d 100644 --- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml +++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml @@ -46,6 +46,7 @@ exception ReferenceToAxiom;; exception ReferenceToVariable;; exception ReferenceToCurrentProof;; exception ReferenceToInductiveDefinition;; +exception RelToHiddenHypothesis;; (* takes a well-typed term *) let whd context = @@ -55,8 +56,9 @@ let whd context = function C.Rel n as t -> (match List.nth context (n-1) with - C.Decl _ -> if l = [] then t else C.Appl (t::l) - | C.Def bo -> whdaux l (S.lift n bo) + Some (C.Decl _) -> if l = [] then t else C.Appl (t::l) + | Some (C.Def bo) -> whdaux l (S.lift n bo) + | None -> raise RelToHiddenHypothesis ) | C.Var uri as t -> (match CicEnvironment.get_cooked_obj uri 0 with @@ -204,14 +206,15 @@ let are_convertible = match (t1,t2) with (C.Rel n1, C.Rel n2) -> n1 = n2 | (C.Var uri1, C.Var uri2) -> U.eq uri1 uri2 - | (C.Meta n1, C.Meta n2) -> n1 = n2 + | (C.Meta (n1,l1), C.Meta (n2,l2)) -> + if n1 = n2 then (assert (l1=l2);true) else false | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *) | (C.Prod (_,s1,t1), C.Prod(_,s2,t2)) -> - aux context s1 s2 && aux ((C.Decl s1)::context) t1 t2 + aux context s1 s2 && aux ((Some (C.Decl s1))::context) t1 t2 | (C.Lambda (_,s1,t1), C.Lambda(_,s2,t2)) -> - aux context s1 s2 && aux ((C.Decl s1)::context) t1 t2 + aux context s1 s2 && aux ((Some (C.Decl s1))::context) t1 t2 | (C.LetIn (_,s1,t1), C.LetIn(_,s2,t2)) -> - aux context s1 s2 && aux ((C.Def s1)::context) t1 t2 + aux context s1 s2 && aux ((Some (C.Def s1))::context) t1 t2 | (C.Appl l1, C.Appl l2) -> (try List.fold_right2 (fun x y b -> aux context x y && b) l1 l2 true @@ -247,8 +250,7 @@ let are_convertible = aux context term1 term2 && List.fold_right2 (fun x y b -> b && aux context x y) pl1 pl2 true | (C.Fix (i1,fl1), C.Fix (i2,fl2)) -> -(*CSC: C.Decl e' giusto? *) - let tys = List.map (function (_,_,ty,_) -> C.Decl ty) fl1 in + let tys = List.map (function (_,_,ty,_) -> Some (C.Decl ty)) fl1 in i1 = i2 && List.fold_right2 (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) b -> @@ -256,8 +258,7 @@ let are_convertible = aux (tys@context) bo1 bo2) fl1 fl2 true | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) -> -(*CSC: C.Decl e' giusto? *) - let tys = List.map (function (_,ty,_) -> C.Decl ty) fl1 in + let tys = List.map (function (_,ty,_) -> Some (C.Decl ty)) fl1 in i1 = i2 && List.fold_right2 (fun (_,ty1,bo1) (_,ty2,bo2) b -> diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml index b683dd258..68276d74b 100644 --- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml +++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml @@ -23,6 +23,9 @@ * http://cs.unibo.it/helm/. *) +exception CannotSubstInMeta;; +exception RelToHiddenHypothesis;; + let lift n = let rec liftaux k = let module C = Cic in @@ -33,7 +36,15 @@ let lift n = else C.Rel (m + n) | C.Var _ as t -> t - | C.Meta _ as t -> t + | C.Meta (i,l) -> + let l' = + List.map + (function + None -> None + | Some t -> Some (liftaux k t) + ) l + in + C.Meta(i,l') | C.Sort _ as t -> t | C.Implicit as t -> t | C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty) @@ -82,7 +93,15 @@ let subst arg = | _ -> C.Rel (n - 1) ) | C.Var _ as t -> t - | C.Meta _ as t -> t + | C.Meta (i, l) as t -> + let l' = + List.map + (function + None -> None + | Some t -> Some (substaux k t) + ) l + in + C.Meta(i,l') | C.Sort _ as t -> t | C.Implicit as t -> t | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty) @@ -151,3 +170,168 @@ let undebrujin_inductive_def uri = Cic.InductiveDefinition (dl', params, n_ind_params) | obj -> obj ;; + +(* l is the relocation list *) + +let lift_meta l t = + let module C = Cic in + if l = [] then t else + let rec aux k = function + C.Rel n as t -> + if n <= k then t else + (try + match List.nth l (n-k-1) with + None -> raise RelToHiddenHypothesis + | Some t -> lift k t + with + (Failure _) -> assert false + ) + | C.Var _ as t -> t + | C.Meta (i,l) -> + let l' = + List.map + (function + None -> None + | Some t -> + try + Some (aux k t) + with + RelToHiddenHypothesis -> None + ) l + in + C.Meta(i,l') + | C.Sort _ as t -> t + | C.Implicit as t -> t + | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) (*CSC ??? *) + | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k + 1) t) + | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k + 1) t) + | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k + 1) t) + | C.Appl l -> C.Appl (List.map (aux k) l) + | C.Const _ as t -> t + | C.Abst _ as t -> t + | C.MutInd _ as t -> t + | C.MutConstruct _ as t -> t + | C.MutCase (sp,cookingsno,i,outt,t,pl) -> + C.MutCase (sp,cookingsno,i,aux k outt, aux k t, + List.map (aux k) pl) + | C.Fix (i,fl) -> + let len = List.length fl in + let substitutedfl = + List.map + (fun (name,i,ty,bo) -> (name, i, aux k ty, aux (k+len) bo)) + fl + in + C.Fix (i, substitutedfl) + | C.CoFix (i,fl) -> + let len = List.length fl in + let substitutedfl = + List.map + (fun (name,ty,bo) -> (name, aux k ty, aux (k+len) bo)) + fl + in + C.CoFix (i, substitutedfl) + in + aux 0 t +;; + +(************************************************************************) +(*CSC: spostare in cic_unification *) + +(* the delift function takes in input an ordered list of integers [n1,...,nk] + and a term t, and relocates rel(nk) to k. Typically, the list of integers + is a parameter of a metavariable occurrence. *) + +exception NotInTheList;; + +let position n = + let rec aux k = + function + [] -> raise NotInTheList + | (Some (Cic.Rel m))::_ when m=n -> k + | _::tl -> aux (k+1) tl in + aux 1 +;; + +let restrict to_be_restricted = + let rec erase i n = + function + [] -> [] + | _::tl when List.mem (n,i) to_be_restricted -> + None::(erase (i+1) n tl) + | he::tl -> he::(erase (i+1) n tl) in + let rec aux = + function + [] -> [] + | (n,context,t)::tl -> (n,erase 1 n context,t)::(aux tl) in + aux +;; + + +let delift context metasenv l t = + let to_be_restricted = ref [] in + let rec deliftaux k = + let module C = Cic in + function + C.Rel m -> + if m <=k then + C.Rel m (*CSC: che succede se c'e' un Def? Dovrebbe averlo gia' *) + (*CSC: deliftato la regola per il LetIn *) + else + (match List.nth context (m-k-1) with + Some (_,C.Def t) -> deliftaux k (lift m t) + | Some (_,C.Decl t) -> + (* It may augment to_be_restricted *) + ignore (deliftaux k (lift m t)) ; + C.Rel ((position (m-k) l) + k) + | None -> raise RelToHiddenHypothesis) + | C.Var _ as t -> t + | C.Meta (i, l1) as t -> + let rec deliftl j = + function + [] -> [] + | None::tl -> None::(deliftl (j+1) tl) + | (Some t)::tl -> + let l1' = (deliftl (j+1) tl) in + try + Some (deliftaux k t)::l1' + with + RelToHiddenHypothesis + | NotInTheList -> + to_be_restricted := (i,j)::!to_be_restricted ; None::l1' + in + let l' = deliftl 1 l1 in + C.Meta(i,l') + | C.Sort _ as t -> t + | C.Implicit as t -> t + | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty) + | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t) + | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t) + | C.LetIn (n,s,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t) + | C.Appl l -> C.Appl (List.map (deliftaux k) l) + | C.Const _ as t -> t + | C.Abst _ as t -> t + | C.MutInd _ as t -> t + | C.MutConstruct _ as t -> t + | C.MutCase (sp,cookingsno,i,outty,t,pl) -> + C.MutCase (sp, cookingsno, i, deliftaux k outty, deliftaux k t, + List.map (deliftaux k) pl) + | C.Fix (i, fl) -> + let len = List.length fl in + let liftedfl = + List.map + (fun (name, i, ty, bo) -> (name, i, deliftaux k ty, deliftaux (k+len) bo)) + fl + in + C.Fix (i, liftedfl) + | C.CoFix (i, fl) -> + let len = List.length fl in + let liftedfl = + List.map + (fun (name, ty, bo) -> (name, deliftaux k ty, deliftaux (k+len) bo)) + fl + in + C.CoFix (i, liftedfl) + in + let res = deliftaux 0 t in + res, restrict !to_be_restricted metasenv +;; diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.mli b/helm/ocaml/cic_proof_checking/cicSubstitution.mli index 72e9a32c2..641d36fee 100644 --- a/helm/ocaml/cic_proof_checking/cicSubstitution.mli +++ b/helm/ocaml/cic_proof_checking/cicSubstitution.mli @@ -25,4 +25,7 @@ val lift : int -> Cic.term -> Cic.term val subst : Cic.term -> Cic.term -> Cic.term +val lift_meta : (Cic.term option) list -> Cic.term -> Cic.term +val delift : + Cic.context -> Cic.metasenv -> (Cic.term option) list -> Cic.term -> Cic.term * Cic.metasenv val undebrujin_inductive_def : UriManager.uri -> Cic.obj -> Cic.obj diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 34eb7d23f..2e8b5585f 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -32,6 +32,8 @@ exception ListTooShort;; exception NotPositiveOccurrences of string;; exception NotWellFormedTypeOfInductiveConstructor of string;; exception WrongRequiredArgument of string;; +exception RelToHiddenHypothesis;; +exception MetasenvInconsistency;; let fdebug = ref 0;; let debug t context = @@ -127,15 +129,15 @@ and does_not_occur context n nn te = | C.Implicit -> true | C.Cast (te,ty) -> does_not_occur context n nn te && does_not_occur context n nn ty - | C.Prod (_,so,dest) -> + | C.Prod (name,so,dest) -> does_not_occur context n nn so && - does_not_occur ((C.Decl so)::context) (n + 1) (nn + 1) dest - | C.Lambda (_,so,dest) -> + does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) dest + | C.Lambda (name,so,dest) -> does_not_occur context n nn so && - does_not_occur ((C.Decl so)::context) (n + 1) (nn + 1) dest - | C.LetIn (_,so,dest) -> + does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) dest + | C.LetIn (name,so,dest) -> does_not_occur context n nn so && - does_not_occur ((C.Def so)::context) (n + 1) (nn + 1) dest + does_not_occur ((Some (name,(C.Def so)))::context) (n + 1) (nn + 1) dest | C.Appl l -> List.fold_right (fun x i -> i && does_not_occur context n nn x) l true | C.Const _ @@ -149,7 +151,9 @@ and does_not_occur context n nn te = let len = List.length fl in let n_plus_len = n + len in let nn_plus_len = nn + len in - let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) fl in + let tys = + List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl + in List.fold_right (fun (_,_,ty,bo) i -> i && does_not_occur context n nn ty && @@ -159,7 +163,9 @@ and does_not_occur context n nn te = let len = List.length fl in let n_plus_len = n + len in let nn_plus_len = nn + len in - let tys = List.map (fun (_,ty,_) -> Cic.Decl ty) fl in + let tys = + List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl + in List.fold_right (fun (_,ty,bo) i -> i && does_not_occur context n nn ty && @@ -214,17 +220,20 @@ and weakly_positive context n nn uri te = | C.Prod (C.Anonimous,source,dest) -> strictly_positive context n nn (subst_inductive_type_with_dummy_mutind source) && - weakly_positive ((C.Decl source)::context) (n + 1) (nn + 1) uri dest + weakly_positive ((Some (C.Anonimous,(C.Decl source)))::context) + (n + 1) (nn + 1) uri dest | C.Prod (name,source,dest) when - does_not_occur ((C.Decl source)::context) 0 n dest -> + does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest -> (* dummy abstraction, so we behave as in the anonimous case *) strictly_positive context n nn (subst_inductive_type_with_dummy_mutind source) && - weakly_positive ((C.Decl source)::context) (n + 1) (nn + 1) uri dest - | C.Prod (_,source,dest) -> + weakly_positive ((Some (name,(C.Decl source)))::context) + (n + 1) (nn + 1) uri dest + | C.Prod (name,source,dest) -> does_not_occur context n nn (subst_inductive_type_with_dummy_mutind source)&& - weakly_positive ((C.Decl source)::context) (n + 1) (nn + 1) uri dest + weakly_positive ((Some (name,(C.Decl source)))::context) + (n + 1) (nn + 1) uri dest | _ -> raise (NotWellFormedTypeOfInductiveConstructor ("Guess where the error is ;-)")) (* instantiate_parameters ps (x1:T1)...(xn:Tn)C *) @@ -247,17 +256,17 @@ and strictly_positive context n nn te = | C.Cast (te,ty) -> (*CSC: bisogna controllare ty????*) strictly_positive context n nn te - | C.Prod (_,so,ta) -> + | C.Prod (name,so,ta) -> does_not_occur context n nn so && - strictly_positive ((C.Decl so)::context) (n+1) (nn+1) ta + strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) ta | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true | C.Appl ((C.MutInd (uri,_,i))::tl) -> - let (ok,paramsno,ity,cl) = + let (ok,paramsno,ity,cl,name) = match CicEnvironment.get_obj uri with C.InductiveDefinition (tl,_,paramsno) -> - let (_,_,ity,cl) = List.nth tl i in - (List.length tl = 1, paramsno, ity, cl) + let (name,_,ity,cl) = List.nth tl i in + (List.length tl = 1, paramsno, ity, cl, name) | _ -> raise(WrongUriToMutualInductiveDefinitions(U.string_of_uri uri)) in let (params,arguments) = split tl paramsno in @@ -273,7 +282,8 @@ and strictly_positive context n nn te = List.fold_right (fun x i -> i && - weakly_positive ((Cic.Decl ity)::context) (n+1) (nn+1) uri x + weakly_positive + ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri x ) cl' true | t -> does_not_occur context n nn t @@ -306,18 +316,20 @@ and are_all_occurrences_positive context uri indparamsno i n nn te = raise (WrongRequiredArgument (UriManager.string_of_uri uri)) | C.Prod (C.Anonimous,source,dest) -> strictly_positive context n nn source && - are_all_occurrences_positive ((C.Decl source)::context) uri indparamsno + are_all_occurrences_positive + ((Some (C.Anonimous,(C.Decl source)))::context) uri indparamsno (i+1) (n + 1) (nn + 1) dest | C.Prod (name,source,dest) when - does_not_occur ((C.Decl source)::context) 0 n dest -> + does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest -> (* dummy abstraction, so we behave as in the anonimous case *) strictly_positive context n nn source && - are_all_occurrences_positive ((C.Decl source)::context) uri indparamsno + are_all_occurrences_positive + ((Some (name,(C.Decl source)))::context) uri indparamsno (i+1) (n + 1) (nn + 1) dest - | C.Prod (_,source,dest) -> + | C.Prod (name,source,dest) -> does_not_occur context n nn source && - are_all_occurrences_positive ((C.Decl source)::context) uri indparamsno - (i+1) (n + 1) (nn + 1) dest + are_all_occurrences_positive ((Some (name,(C.Decl source)))::context) + uri indparamsno (i+1) (n + 1) (nn + 1) dest | _ -> raise (NotWellFormedTypeOfInductiveConstructor (UriManager.string_of_uri uri)) (*CSC: cambiare il nome, torna unit! *) @@ -339,7 +351,8 @@ and cooked_mutual_inductive_defs uri = (*CSC: siamo sicuri che non debba fare anche un List.rev? Il bug *) (*CSC: si manifesterebbe solamene con tipi veramente mutualmente *) (*CSC: induttivi... *) - let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) itl in + let tys = + List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in let _ = List.fold_right (fun (_,_,_,cl) i -> @@ -425,9 +438,9 @@ and recursive_args context n nn te = | C.Sort _ | C.Implicit | C.Cast _ (*CSC ??? *) -> raise (Impossible 3) (* due to type-checking *) - | C.Prod (_,so,de) -> + | C.Prod (name,so,de) -> (not (does_not_occur context n nn so)) :: - (recursive_args ((C.Decl so)::context) (n+1) (nn + 1) de) + (recursive_args ((Some (name,(C.Decl so)))::context) (n+1) (nn + 1) de) | C.Lambda _ | C.LetIn _ -> raise (Impossible 4) (* due to type-checking *) | C.Appl _ -> [] @@ -444,7 +457,7 @@ and get_new_safes context p c rl safes n nn x = let module U = UriManager in let module R = CicReduction in match (R.whd context c, R.whd context p, rl) with - (C.Prod (_,so,ta1), C.Lambda (_,_,ta2), b::tl) -> + (C.Prod (_,so,ta1), C.Lambda (name,_,ta2), b::tl) -> (* we are sure that the two sources are convertible because we *) (* have just checked this. So let's go along ... *) let safes' = @@ -453,8 +466,8 @@ and get_new_safes context p c rl safes n nn x = let safes'' = if b then 1::safes' else safes' in - get_new_safes ((C.Decl so)::context) ta2 ta1 tl safes'' (n+1) (nn+1) - (x+1) + get_new_safes ((Some (name,(C.Decl so)))::context) + ta2 ta1 tl safes'' (n+1) (nn+1) (x+1) | (C.Prod _, (C.MutConstruct _ as e), _) | (C.Prod _, (C.Rel _ as e), _) | (C.MutInd _, e, []) @@ -472,8 +485,8 @@ and split_prods context n te = let module R = CicReduction in match (n, R.whd context te) with (0, _) -> context,te - | (n, C.Prod (_,so,ta)) when n > 0 -> - split_prods ((C.Decl so)::context) (n - 1) ta + | (n, C.Prod (name,so,ta)) when n > 0 -> + split_prods ((Some (name,(C.Decl so)))::context) (n - 1) ta | (_, _) -> raise (Impossible 8) and eat_lambdas context n te = @@ -481,8 +494,10 @@ and eat_lambdas context n te = let module R = CicReduction in match (n, R.whd context te) with (0, _) -> (te, 0, context) - | (n, C.Lambda (_,so,ta)) when n > 0 -> - let (te, k, context') = eat_lambdas ((C.Decl so)::context) (n - 1) ta in + | (n, C.Lambda (name,so,ta)) when n > 0 -> + let (te, k, context') = + eat_lambdas ((Some (name,(C.Decl so)))::context) (n - 1) ta + in (te, k + 1, context') | (_, _) -> raise (Impossible 9) @@ -508,14 +523,14 @@ and check_is_really_smaller_arg context n nn kl x safes te = check_is_really_smaller_arg (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta*) | C.Prod _ -> raise (Impossible 10) - | C.Lambda (_,so,ta) -> + | C.Lambda (name,so,ta) -> check_is_really_smaller_arg context n nn kl x safes so && - check_is_really_smaller_arg ((C.Decl so)::context) (n+1) (nn+1) kl (x+1) - (List.map (fun x -> x + 1) safes) ta - | C.LetIn (_,so,ta) -> + check_is_really_smaller_arg ((Some (name,(C.Decl so)))::context) + (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta + | C.LetIn (name,so,ta) -> check_is_really_smaller_arg context n nn kl x safes so && - check_is_really_smaller_arg ((C.Def so)::context) (n+1) (nn+1) kl (x+1) - (List.map (fun x -> x + 1) safes) ta + check_is_really_smaller_arg ((Some (name,(C.Def so)))::context) + (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta | C.Appl (he::_) -> (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *) (*CSC: solo perche' non abbiamo trovato controesempi *) @@ -531,7 +546,9 @@ and check_is_really_smaller_arg context n nn kl x safes te = let (isinductive,paramsno,cl) = match CicEnvironment.get_obj uri with C.InductiveDefinition (tl,_,paramsno) -> - let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) tl in + let tys = + List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl + in let (_,isinductive,_,cl) = List.nth tl i in let cl' = List.map @@ -568,7 +585,9 @@ and check_is_really_smaller_arg context n nn kl x safes te = match CicEnvironment.get_obj uri with C.InductiveDefinition (tl,_,paramsno) -> let (_,isinductive,_,cl) = List.nth tl i in - let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) tl in + let tys = + List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl + in let cl' = List.map (fun (id,ty,r) -> @@ -612,8 +631,7 @@ and check_is_really_smaller_arg context n nn kl x safes te = let n_plus_len = n + len and nn_plus_len = nn + len and x_plus_len = x + len - (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) - and tys = List.map (fun (_,_,ty,_) -> C.Decl ty) fl + and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl and safes' = List.map (fun x -> x + len) safes in List.fold_right (fun (_,_,ty,bo) i -> @@ -626,8 +644,7 @@ and check_is_really_smaller_arg context n nn kl x safes te = let n_plus_len = n + len and nn_plus_len = nn + len and x_plus_len = x + len - (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) - and tys = List.map (fun (_,ty,_) -> C.Decl ty) fl + and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl and safes' = List.map (fun x -> x + len) safes in List.fold_right (fun (_,ty,bo) i -> @@ -643,8 +660,9 @@ and guarded_by_destructors context n nn kl x safes = C.Rel m when m > n && m <= nn -> false | C.Rel n -> (match List.nth context (n-1) with - C.Decl _ -> true - | C.Def bo -> guarded_by_destructors context n nn kl x safes bo + Some (_,C.Decl _) -> true + | Some (_,C.Def bo) -> guarded_by_destructors context n nn kl x safes bo + | None -> raise RelToHiddenHypothesis ) | C.Var _ | C.Meta _ @@ -653,18 +671,18 @@ and guarded_by_destructors context n nn kl x safes = | C.Cast (te,ty) -> guarded_by_destructors context n nn kl x safes te && guarded_by_destructors context n nn kl x safes ty - | C.Prod (_,so,ta) -> + | C.Prod (name,so,ta) -> guarded_by_destructors context n nn kl x safes so && - guarded_by_destructors ((C.Decl so)::context) (n+1) (nn+1) kl (x+1) - (List.map (fun x -> x + 1) safes) ta - | C.Lambda (_,so,ta) -> + guarded_by_destructors ((Some (name,(C.Decl so)))::context) + (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta + | C.Lambda (name,so,ta) -> guarded_by_destructors context n nn kl x safes so && - guarded_by_destructors ((C.Decl so)::context) (n+1) (nn+1) kl (x+1) - (List.map (fun x -> x + 1) safes) ta - | C.LetIn (_,so,ta) -> + guarded_by_destructors ((Some (name,(C.Decl so)))::context) + (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta + | C.LetIn (name,so,ta) -> guarded_by_destructors context n nn kl x safes so && - guarded_by_destructors ((C.Def so)::context) (n+1) (nn+1) kl (x+1) - (List.map (fun x -> x + 1) safes) ta + guarded_by_destructors ((Some (name,(C.Def so)))::context) + (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> let k = List.nth kl (m - n - 1) in if not (List.length tl > k) then false @@ -689,7 +707,9 @@ and guarded_by_destructors context n nn kl x safes = match CicEnvironment.get_obj uri with C.InductiveDefinition (tl,_,paramsno) -> let (_,isinductive,_,cl) = List.nth tl i in - let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) tl in + let tys = + List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl + in let cl' = List.map (fun (id,ty,r) -> @@ -730,7 +750,9 @@ and guarded_by_destructors context n nn kl x safes = match CicEnvironment.get_obj uri with C.InductiveDefinition (tl,_,paramsno) -> let (_,isinductive,_,cl) = List.nth tl i in - let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) tl in + let tys = + List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl + in let cl' = List.map (fun (id,ty,r) -> @@ -783,8 +805,7 @@ and guarded_by_destructors context n nn kl x safes = let n_plus_len = n + len and nn_plus_len = nn + len and x_plus_len = x + len - (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) - and tys = List.map (fun (_,_,ty,_) -> C.Decl ty) fl + and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl and safes' = List.map (fun x -> x + len) safes in List.fold_right (fun (_,_,ty,bo) i -> @@ -797,8 +818,7 @@ and guarded_by_destructors context n nn kl x safes = let n_plus_len = n + len and nn_plus_len = nn + len and x_plus_len = x + len - (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) - and tys = List.map (fun (_,ty,_) -> C.Decl ty) fl + and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl and safes' = List.map (fun x -> x + len) safes in List.fold_right (fun (_,ty,bo) i -> @@ -828,10 +848,10 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = | C.Prod _ | C.LetIn _ -> raise (Impossible 17) (* the term has just been type-checked *) - | C.Lambda (_,so,de) -> + | C.Lambda (name,so,de) -> does_not_occur context n nn so && - guarded_by_constructors ((C.Decl so)::context) (n + 1) (nn + 1) h de args - coInductiveTypeURI + guarded_by_constructors ((Some (name,(C.Decl so)))::context) + (n + 1) (nn + 1) h de args coInductiveTypeURI | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> h && List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true @@ -854,8 +874,8 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = does_not_occur context n nn te | C.Implicit | C.Cast _ -> raise (Impossible 24) (* due to type-checking *) - | C.Prod (_,so,de) -> - analyse_branch ((C.Decl so)::context) de te + | C.Prod (name,so,de) -> + analyse_branch ((Some (name,(C.Decl so)))::context) de te | C.Lambda _ | C.LetIn _ -> raise (Impossible 25) (* due to type-checking *) | C.Appl ((C.MutInd (uri,_,_))::tl) as ty @@ -886,13 +906,14 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = | C.Sort _ | C.Implicit | C.Cast _ -> raise (Impossible 29) (* due to type-checking *) - | C.Prod (_,so,de) -> + | C.Prod (name,so,de) -> begin match l with [] -> true | he::tl -> analyse_branch context so he && - analyse_instantiated_type ((C.Decl so)::context) de tl + analyse_instantiated_type ((Some (name,(C.Decl so)))::context) + de tl end | C.Lambda _ | C.LetIn _ -> raise (Impossible 30) (* due to type-checking *) @@ -940,7 +961,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = let n_plus_len = n + len and nn_plus_len = nn + len (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) - and tys = List.map (fun (_,ty,_) -> C.Decl ty) fl in + and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in List.fold_right (fun (_,ty,bo) i -> i && does_not_occur context n nn ty && @@ -975,7 +996,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = let n_plus_len = n + len and nn_plus_len = nn + len (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) - and tys = List.map (fun (_,_,ty,_) -> C.Decl ty) fl in + and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in List.fold_right (fun (_,_,ty,bo) i -> i && does_not_occur context n nn ty && @@ -986,7 +1007,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = let n_plus_len = n + len and nn_plus_len = nn + len (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) - and tys = List.map (fun (_,ty,_) -> C.Decl ty) fl in + and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in List.fold_right (fun (_,ty,bo) i -> i && does_not_occur context n nn ty && @@ -1017,7 +1038,9 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 = | (C.Sort C.Set, C.Sort C.Type) when need_dummy -> (match CicEnvironment.get_obj uri with C.InductiveDefinition (itl,_,paramsno) -> - let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) itl in + let tys = + List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl + in let (_,_,_,cl) = List.nth itl i in List.fold_right (fun (_,x,_) i -> i && is_small tys paramsno x) cl true @@ -1025,11 +1048,11 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 = raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) ) | (C.Sort C.Type, C.Sort _) when need_dummy -> true - | (C.Sort C.Prop, C.Prod (_,so,ta)) when not need_dummy -> + | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy -> let res = CicReduction.are_convertible context so ind in res && - (match CicReduction.whd ((C.Decl so)::context) ta with + (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with C.Sort C.Prop -> true | C.Sort C.Set -> (match CicEnvironment.get_obj uri with @@ -1043,18 +1066,21 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 = ) | _ -> false ) - | (C.Sort C.Set, C.Prod (_,so,ta)) when not need_dummy -> + | (C.Sort C.Set, C.Prod (name,so,ta)) when not need_dummy -> let res = CicReduction.are_convertible context so ind in res && - (match CicReduction.whd ((C.Decl so)::context) ta with + (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with C.Sort C.Prop | C.Sort C.Set -> true | C.Sort C.Type -> (match CicEnvironment.get_obj uri with C.InductiveDefinition (itl,_,paramsno) -> let (_,_,_,cl) = List.nth itl i in - let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) itl in + let tys = + List.map + (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl + in List.fold_right (fun (_,x,_) i -> i && is_small tys paramsno x) cl true | _ -> @@ -1084,12 +1110,46 @@ and type_of_branch context argsno need_dummy outtype term constype = else C.Appl (outtype::arguments@(if need_dummy then [] else [term])) | C.Prod (name,so,de) -> - C.Prod (C.Anonimous,so,type_of_branch ((C.Decl so)::context) argsno - need_dummy (CicSubstitution.lift 1 outtype) + C.Prod (C.Anonimous,so,type_of_branch + ((Some (name,(C.Decl so)))::context) argsno need_dummy + (CicSubstitution.lift 1 outtype) (C.Appl [CicSubstitution.lift 1 term ; C.Rel 1]) de) | _ -> raise (Impossible 20) - - + +(* 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 *) + +and check_metasenv_consistency metasenv context canonical_context l = + let module C = Cic in + let module R = CicReduction in + let module S = CicSubstitution in + let lifted_canonical_context = + let rec aux i = + function + [] -> [] + | (Some (n,C.Decl t))::tl -> + (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl) + | (Some (n,C.Def t))::tl -> + (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl) + | None::tl -> None::(aux (i+1) tl) + in + aux 1 canonical_context + in + List.iter2 + (fun t ct -> + let res = + match (t,ct) with + _,None -> true + | Some t,Some (_,C.Def ct) -> + R.are_convertible context t ct + | Some t,Some (_,C.Decl ct) -> + R.are_convertible context (type_of_aux' metasenv context t) ct + | _, _ -> false + in + if not res then raise MetasenvInconsistency + ) l lifted_canonical_context + (* type_of_aux' is just another name (with a different scope) for type_of_aux *) and type_of_aux' metasenv context t = let rec type_of_aux context = @@ -1101,8 +1161,9 @@ and type_of_aux' metasenv context t = C.Rel n -> (try match List.nth context (n - 1) with - C.Decl t -> S.lift n t - | C.Def bo -> type_of_aux context (S.lift n bo) + Some (_,C.Decl t) -> S.lift n t + | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo) + | None -> raise RelToHiddenHypothesis with _ -> raise (NotWellTyped "Not a close term") ) @@ -1111,27 +1172,33 @@ and type_of_aux' metasenv context t = let ty = type_of_variable uri in decr fdebug ; ty - | C.Meta n -> List.assoc n metasenv + | C.Meta (n,l) -> + let (_,canonical_context,ty) = + List.find (function (m,_,_) -> n = m) 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!!! *) | C.Implicit -> raise (Impossible 21) | C.Cast (te,ty) -> let _ = type_of_aux context ty in if R.are_convertible context (type_of_aux context te) ty then ty else raise (NotWellTyped "Cast") - | C.Prod (_,s,t) -> + | C.Prod (name,s,t) -> let sort1 = type_of_aux context s - and sort2 = type_of_aux ((C.Decl s)::context) t in - sort_of_prod (sort1,sort2) + and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in + sort_of_prod context (name,s) (sort1,sort2) | C.Lambda (n,s,t) -> let sort1 = type_of_aux context s - and type2 = type_of_aux ((C.Decl s)::context) t in - let sort2 = type_of_aux ((C.Decl s)::context) type2 in + and type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t in + let sort2 = type_of_aux ((Some (n,(C.Decl s)))::context) type2 in (* only to check if the product is well-typed *) - let _ = sort_of_prod (sort1,sort2) in + let _ = sort_of_prod context (n,s) (sort1,sort2) in C.Prod (n,s,type2) | C.LetIn (n,s,t) -> - let t' = CicSubstitution.subst s t in - type_of_aux context t' + (* only to check if s is well-typed *) + let _ = type_of_aux context s in + C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t) | C.Appl (he::tl) when List.length tl > 0 -> let hetype = type_of_aux context he and tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in @@ -1158,8 +1225,8 @@ and type_of_aux' metasenv context t = let rec guess_args context t = match CicReduction.whd context t with C.Sort _ -> (true, 0) - | C.Prod (_, s, t) -> - let (b, n) = guess_args ((C.Decl s)::context) t in + | C.Prod (name, s, t) -> + let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in if n = 0 then (* last prod before sort *) match CicReduction.whd context s with @@ -1243,8 +1310,9 @@ and type_of_aux' metasenv context t = let types_times_kl = List.rev (List.map - (fun (_,k,ty,_) -> - let _ = type_of_aux context ty in (C.Decl ty,k)) fl) + (fun (n,k,ty,_) -> + let _ = type_of_aux context ty in + (Some (C.Name n,(C.Decl ty)),k)) fl) in let (types,kl) = List.split types_times_kl in let len = List.length types in @@ -1276,7 +1344,8 @@ and type_of_aux' metasenv context t = let types = List.rev (List.map - (fun (_,ty,_) -> let _ = type_of_aux context ty in C.Decl ty) fl) + (fun (n,ty,_) -> + let _ = type_of_aux context ty in Some (C.Name n,(C.Decl ty))) fl) in let len = List.length types in List.iter @@ -1287,7 +1356,7 @@ and type_of_aux' metasenv context t = then begin (* let's control that the returned type is coinductive *) - match returns_a_coinductive ty with + match returns_a_coinductive context ty with None -> raise(NotWellTyped "CoFix: does not return a coinductive type") | Some uri -> @@ -1306,10 +1375,10 @@ and type_of_aux' metasenv context t = let (_,ty,_) = List.nth fl i in ty - and sort_of_prod (t1, t2) = + and sort_of_prod context (name,s) (t1, t2) = let module C = Cic in let t1' = CicReduction.whd context t1 in - let t2' = CicReduction.whd context t2 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) -> (* different from Coq manual!!! *) @@ -1343,7 +1412,7 @@ and type_of_aux' metasenv context t = | _ -> raise (NotWellTyped "Appl: wrong Prod-type") ) - and returns_a_coinductive ty = + and returns_a_coinductive context ty = let module C = Cic in match CicReduction.whd context ty with C.MutInd (uri,cookingsno,i) -> @@ -1365,7 +1434,8 @@ and type_of_aux' metasenv context t = raise (WrongUriToMutualInductiveDefinitions (UriManager.string_of_uri uri)) ) - | C.Prod (_,_,de) -> returns_a_coinductive de + | C.Prod (n,so,de) -> + returns_a_coinductive ((Some (n,C.Decl so))::context) de | _ -> None in @@ -1384,11 +1454,11 @@ and is_small context paramsno c = let rec is_small_aux context c = let module C = Cic in match CicReduction.whd context c with - C.Prod (_,so,de) -> + C.Prod (n,so,de) -> (*CSC: [] is an empty metasenv. Is it correct? *) let s = type_of_aux' [] context so in (s = C.Sort C.Prop || s = C.Sort C.Set) && - is_small_aux ((C.Decl so)::context) de + is_small_aux ((Some (n,(C.Decl so)))::context) de | _ -> true (*CSC: we trust the type-checker *) in let (context',dx) = split_prods context paramsno c in diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli index 93f956143..a18d651f6 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli @@ -36,4 +36,4 @@ val typecheck : UriManager.uri -> unit (* used only in the toplevel *) (* type_of_aux' metasenv context term *) val type_of_aux': - (int * Cic.term) list -> Cic.context -> Cic.term -> Cic.term + Cic.metasenv -> Cic.context -> Cic.term -> Cic.term diff --git a/helm/ocaml/cic_textual_parser/cicTextualLexer.mll b/helm/ocaml/cic_textual_parser/cicTextualLexer.mll index 8c1a5b4ae..31878bfe6 100644 --- a/helm/ocaml/cic_textual_parser/cicTextualLexer.mll +++ b/helm/ocaml/cic_textual_parser/cicTextualLexer.mll @@ -80,6 +80,8 @@ rule token = | '?' { IMPLICIT } | '(' { LPAREN } | ')' { RPAREN } + | '[' { LBRACKET } + | ']' { RBRACKET } | '{' { LCURLY } | '}' { RCURLY } | ';' { SEMICOLON } @@ -88,5 +90,6 @@ rule token = | ':' { COLON } | '.' { DOT } | "->" { ARROW } + | "_" { NONE } | eof { EOF } {} diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly index f3dc1b05e..3f6afc79a 100644 --- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly +++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly @@ -37,7 +37,7 @@ let rec aux i = function [] -> raise Not_found - | he::_ when he = e -> i + | (Some he)::_ when he = e -> i | _::tl -> aux (i+1) tl in aux 1 @@ -55,8 +55,8 @@ %token INDTYURI %token INDCONURI %token ALIAS -%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT -%token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW EOF +%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT NONE +%token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF %right ARROW %start main %type main @@ -156,7 +156,7 @@ expr2: | PROP { Sort Prop } | TYPE { Sort Type } | LPAREN expr CAST expr RPAREN { Cast ($2,$4) } - | META { Meta $1 } + | META LBRACKET substitutionlist RBRACKET { Meta ($1, $3) } | LPAREN expr expr exprlist RPAREN { Appl ([$2;$3]@$4) } ; expr : @@ -174,7 +174,7 @@ expr : ; fixheader: FIX ID LCURLY fixfunsdecl RCURLY - { let bs = List.rev_map (function (name,_,_) -> Name name) $4 in + { let bs = List.rev_map (function (name,_,_) -> Some (Name name)) $4 in CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ; $2,$4 } @@ -187,7 +187,7 @@ fixfunsdecl: ; cofixheader: COFIX ID LCURLY cofixfunsdecl RCURLY - { let bs = List.rev_map (function (name,_) -> Name name) $4 in + { let bs = List.rev_map (function (name,_) -> Some (Name name)) $4 in CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ; $2,$4 } @@ -200,23 +200,23 @@ cofixfunsdecl: ; pihead: PROD ID COLON expr DOT - { CicTextualParser0.binders := (Name $2)::!CicTextualParser0.binders ; + { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders; (Cic.Name $2, $4) } | expr2 ARROW - { CicTextualParser0.binders := Anonimous::!CicTextualParser0.binders ; + { CicTextualParser0.binders := (Some Anonimous)::!CicTextualParser0.binders ; (Anonimous, $1) } | LPAREN expr RPAREN ARROW - { CicTextualParser0.binders := Anonimous::!CicTextualParser0.binders ; + { CicTextualParser0.binders := (Some Anonimous)::!CicTextualParser0.binders ; (Anonimous, $2) } ; lambdahead: LAMBDA ID COLON expr DOT - { CicTextualParser0.binders := (Name $2)::!CicTextualParser0.binders ; + { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ; (Cic.Name $2, $4) } ; letinhead: LAMBDA ID LETIN expr DOT - { CicTextualParser0.binders := (Name $2)::!CicTextualParser0.binders ; + { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ; (Cic.Name $2, $4) } ; branches: @@ -232,6 +232,11 @@ exprseplist: expr { [$1] } | expr SEMICOLON exprseplist { $1::$3 } ; +substitutionlist: + { [] } + | expr SEMICOLON substitutionlist { (Some $1)::$3 } + | NONE SEMICOLON substitutionlist { None::$3 } +; alias: ALIAS ID CONURI { let cookingno = get_cookingno $3 in @@ -245,3 +250,6 @@ alias: Hashtbl.add uri_of_id_map $2 (Cic.MutConstruct (uri, cookingno, indno ,consno)) } + + + diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml index e89c00d22..7a338c249 100644 --- a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml +++ b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml @@ -26,4 +26,4 @@ exception Eof;; let current_uri = ref (UriManager.uri_of_string "cic:/dummy.con");; -let binders = ref ([] : Cic.name list);; +let binders = ref ([] : (Cic.name option) list);; diff --git a/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli b/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli index 7364eb6fc..0ab69cdd5 100644 --- a/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli +++ b/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli @@ -24,6 +24,6 @@ *) val main : - current_uri:(UriManager.uri) -> context:(Cic.name list) -> + current_uri:(UriManager.uri) -> context:((Cic.name option) list) -> (Lexing.lexbuf -> CicTextualParser.token) -> Lexing.lexbuf -> Cic.term option diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 4126d0446..2f27bea85 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -26,103 +26,63 @@ exception UnificationFailed;; exception Free;; exception OccurCheck;; +exception RelToHiddenHypothesis;; +exception OpenTerm;; type substitution = (int * Cic.term) list -(*CSC: Hhhmmm. Forse dovremmo spostarla in CicSubstitution dove si trova la *) -(*CSC: lift? O creare una proofEngineSubstitution? *) -(* the function delift n m un-lifts a lambda term m of n level of abstractions. - It returns an exception Free if M contains a free variable in the range 1--n *) -let delift n = - let rec deliftaux k = - let module C = Cic in - function - C.Rel m -> - if m < k then C.Rel m else - if m < k+n then raise Free - else C.Rel (m - n) - | C.Var _ as t -> t - | C.Meta _ as t -> t - | C.Sort _ as t -> t - | C.Implicit as t -> t - | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty) - | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t) - | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t) - | C.LetIn (n,s,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t) - | C.Appl l -> C.Appl (List.map (deliftaux k) l) - | C.Const _ as t -> t - | C.Abst _ as t -> t - | C.MutInd _ as t -> t - | C.MutConstruct _ as t -> t - | C.MutCase (sp,cookingsno,i,outty,t,pl) -> - C.MutCase (sp, cookingsno, i, deliftaux k outty, deliftaux k t, - List.map (deliftaux k) pl) - | C.Fix (i, fl) -> - let len = List.length fl in - let liftedfl = - List.map - (fun (name, i, ty, bo) -> (name, i, deliftaux k ty, deliftaux (k+len) bo)) - fl - in - C.Fix (i, liftedfl) - | C.CoFix (i, fl) -> - let len = List.length fl in - let liftedfl = - List.map - (fun (name, ty, bo) -> (name, deliftaux k ty, deliftaux (k+len) bo)) - fl - in - C.CoFix (i, liftedfl) - in - if n = 0 then - (function t -> t) - else - deliftaux 1 -;; - (* NUOVA UNIFICAZIONE *) (* A substitution is a (int * Cic.term) list that associates a metavariable i with its body. A metaenv is a (int * Cic.term) list that associate a metavariable i with is type. - fo_unif_new takes a metasenv, a context, - two terms t1 and t2 and gives back a new - substitution which is _NOT_ unwinded. It must be unwinded before + fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back + a new substitution which is _NOT_ unwinded. It must be unwinded before applying it. *) let fo_unif_new metasenv context t1 t2 = let module C = Cic in let module R = CicReduction in let module S = CicSubstitution in - let rec fo_unif_aux subst k t1 t2 = + let rec fo_unif_aux subst context metasenv t1 t2 = match (t1, t2) with - (C.Meta n, C.Meta m) -> if n == m then subst - else let subst'= - let tn = try List.assoc n subst - with Not_found -> C.Meta n in - let tm = try List.assoc m subst - with Not_found -> C.Meta m in - (match (tn, tm) with - (C.Meta n, C.Meta m) -> if n==m then subst - else if n (n, tm)::subst - | (tn, C.Meta m) -> (m, tn)::subst - | (tn,tm) -> fo_unif_aux subst 0 tn tm) in - (* unify types first *) - let tyn = List.assoc n metasenv in - let tym = List.assoc m metasenv in - fo_unif_aux subst' 0 tyn tym - | (C.Meta n, t) - | (t, C.Meta n) -> (* unify types first *) - let t' = delift k t in - let subst' = - (try fo_unif_aux subst 0 (List.assoc n subst) t' - with Not_found -> (n, t')::subst) in - let tyn = List.assoc n metasenv in - let tyt = CicTypeChecker.type_of_aux' metasenv context t' in - fo_unif_aux subst' 0 tyn tyt + (C.Meta (n,ln), C.Meta (m,lm)) when n=m -> + let ok = + List.fold_left2 + (fun b t1 t2 -> + b && + match t1,t2 with + None,_ + | _,None -> true + | Some t1', Some t2' -> + (* First possibility: restriction *) + (* Second possibility: unification *) + (* Third possibility: convertibility *) + R.are_convertible context t1' t2' + ) true ln lm + in + if ok then subst,metasenv else + raise UnificationFailed + | (C.Meta (n,l), C.Meta (m,_)) when n>m -> + fo_unif_aux subst context metasenv t2 t1 + | (C.Meta (n,l), t) + | (t, C.Meta (n,l)) -> + let subst',metasenv' = + try + let oldt = (List.assoc n subst) in + let lifted_oldt = S.lift_meta l oldt in + fo_unif_aux subst context metasenv lifted_oldt t + with Not_found -> +prerr_endline ("DELIFT2(" ^ CicPp.ppterm t ^ ")") ; flush stderr ; +List.iter (function (Some t) -> prerr_endline ("l: " ^ CicPp.ppterm t) | None -> prerr_endline " _ ") l ; flush stderr ; +prerr_endline " m=n) metasenv' in + let tyt = CicTypeChecker.type_of_aux' metasenv' context t in + fo_unif_aux subst' context metasenv' (S.lift_meta l meta_type) tyt | (C.Rel _, _) | (_, C.Rel _) | (C.Var _, _) @@ -130,32 +90,38 @@ let fo_unif_new metasenv context t1 t2 = | (C.Sort _ ,_) | (_, C.Sort _) | (C.Implicit, _) - | (_, C.Implicit) -> if R.are_convertible context t1 t2 then subst - else raise UnificationFailed - | (C.Cast (te,ty), t2) -> fo_unif_aux subst k te t2 - | (t1, C.Cast (te,ty)) -> fo_unif_aux subst k t1 te - | (C.Prod (_,s1,t1), C.Prod (_,s2,t2)) -> - let subst' = fo_unif_aux subst k s1 s2 in - fo_unif_aux subst' (k+1) t1 t2 - | (C.Lambda (_,s1,t1), C.Lambda (_,s2,t2)) -> - let subst' = fo_unif_aux subst k s1 s2 in - fo_unif_aux subst' (k+1) t1 t2 - | (C.LetIn (_,s1,t1), t2) -> fo_unif_aux subst k (S.subst s1 t1) t2 - | (t1, C.LetIn (_,s2,t2)) -> fo_unif_aux subst k t1 (S.subst s2 t2) + | (_, C.Implicit) -> + if R.are_convertible context t1 t2 then subst, metasenv + else raise UnificationFailed + | (C.Cast (te,ty), t2) -> fo_unif_aux subst context metasenv te t2 + | (t1, C.Cast (te,ty)) -> fo_unif_aux subst context metasenv t1 te + | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> + let subst',metasenv' = fo_unif_aux subst context metasenv s1 s2 in + fo_unif_aux subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 + | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) -> + let subst',metasenv' = fo_unif_aux subst context metasenv s1 s2 in + fo_unif_aux subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 + | (C.LetIn (_,s1,t1), t2) + | (t2, C.LetIn (_,s1,t1)) -> + fo_unif_aux 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 = function - [],_ - | _,[] -> assert false - | ([h1],[h2]) -> fo_unif_aux subst k h1 h2 - | ([h],l) - | (l,[h]) -> fo_unif_aux subst k h (C.Appl l) - | ((h1::l1),(h2::l2)) -> - let subst' = fo_unif_aux subst k h1 h2 in - fo_unif_l subst' (l1,l2) - in - fo_unif_l subst (lr1, lr2) + let lr1 = List.rev l1 in + let lr2 = List.rev l2 in + let rec fo_unif_l subst metasenv = function + [],_ + | _,[] -> assert false + | ([h1],[h2]) -> + fo_unif_aux subst context metasenv h1 h2 + | ([h],l) + | (l,[h]) -> + fo_unif_aux subst context metasenv h (C.Appl (List.rev l)) + | ((h1::l1),(h2::l2)) -> + let subst', metasenv' = + fo_unif_aux subst context metasenv h1 h2 + in + fo_unif_l subst' metasenv' (l1,l2) + in + fo_unif_l subst metasenv (lr1, lr2) | (C.Const _, _) | (_, C.Const _) | (C.Abst _, _) @@ -163,94 +129,258 @@ let fo_unif_new metasenv context t1 t2 = | (C.MutInd _, _) | (_, C.MutInd _) | (C.MutConstruct _, _) - | (_, C.MutConstruct _) -> if R.are_convertible context t1 t2 then subst - else raise UnificationFailed + | (_, C.MutConstruct _) -> + if R.are_convertible context t1 t2 then subst, metasenv + else raise UnificationFailed | (C.MutCase (_,_,_,outt1,t1,pl1), C.MutCase (_,_,_,outt2,t2,pl2))-> - let subst' = fo_unif_aux subst k outt1 outt2 in - let subst'' = fo_unif_aux subst' k t1 t2 in - List.fold_left2 (function subst -> fo_unif_aux subst k) subst'' pl1 pl2 + let subst', metasenv' = + fo_unif_aux subst context metasenv outt1 outt2 in + let subst'',metasenv'' = + fo_unif_aux subst' context metasenv' t1 t2 in + List.fold_left2 + (function (subst,metasenv) -> + fo_unif_aux subst context metasenv + ) (subst'',metasenv'') pl1 pl2 | (C.Fix _, _) | (_, C.Fix _) | (C.CoFix _, _) - | (_, C.CoFix _) -> if R.are_convertible context t1 t2 then subst - else raise UnificationFailed + | (_, C.CoFix _) -> + if R.are_convertible context t1 t2 then subst, metasenv + else raise UnificationFailed | (_,_) -> raise UnificationFailed - in fo_unif_aux [] 0 t1 t2;; + in fo_unif_aux [] context metasenv t1 t2;; + +(*CSC: ??????????????? +(* m is the index of a metavariable to restrict, k is nesting depth +of the occurrence m, and l is its relocation list. canonical_context +is the context of the metavariable we are instantiating - containing +m - Only rel in the domain of canonical_context are accessible. +This function takes in input a metasenv and gives back a metasenv. +A rel(j) in the canonical context of m, is rel(List.nth l j) for the +instance of m under consideration, that is rel (List.nth l j) - k +in canonical_context. *) + +let restrict canonical_context m k l = + let rec erase i = + function + [] -> [] + | None::tl -> None::(erase (i+1) tl) + | he::tl -> + let i' = (List.nth l (i-1)) in + if i' <= k + then he::(erase (i+1) tl) (* local variable *) + else + let acc = + (try List.nth canonical_context (i'-k-1) + with Failure _ -> None) in + if acc = None + then None::(erase (i+1) tl) + else he::(erase (i+1) tl) in + let rec aux = + function + [] -> [] + | (n,context,t)::tl when n=m -> (n,erase 1 context,t)::tl + | hd::tl -> hd::(aux tl) + in + aux +;; + + +let check_accessibility metasenv i = + let module C = Cic in + let module S = CicSubstitution in + let (_,canonical_context,_) = + List.find (function (m,_,_) -> m=i) metasenv in + List.map + (function t -> + let = + S.delift canonical_context metasenv ? t + ) canonical_context +CSCSCS -(* unwind mgu mark m applies mgu to the term m; mark is an array of integers -mark.(n) = 0 if the term has not been unwinded, is 2 if it is under uwinding, -and is 1 if it has been succesfully unwinded. Meeting the value 2 during -the computation is an error: occur-check *) -let unwind subst unwinded t = + + let rec aux metasenv k = + function + C.Rel i -> + if i <= k then + metasenv + else + (try + match List.nth canonical_context (i-k-1) with + Some (_,C.Decl t) + | Some (_,C.Def t) -> aux metasenv k (S.lift i t) + | None -> raise RelToHiddenHypothesis + with + Failure _ -> raise OpenTerm + ) + | C.Var _ -> metasenv + | C.Meta (i,l) -> restrict canonical_context i k l metasenv + | C.Sort _ -> metasenv + | C.Implicit -> metasenv + | C.Cast (te,ty) -> + let metasenv' = aux metasenv k te in + aux metasenv' k ty + | C.Prod (_,s,t) + | C.Lambda (_,s,t) + | C.LetIn (_,s,t) -> + let metasenv' = aux metasenv k s in + aux metasenv' (k+1) t + | C.Appl l -> + List.fold_left + (function metasenv -> aux metasenv k) metasenv l + | C.Const _ + | C.Abst _ + | C.MutInd _ + | C.MutConstruct _ -> metasenv + | C.MutCase (_,_,_,outty,t,pl) -> + let metasenv' = aux metasenv k outty in + let metasenv'' = aux metasenv' k t in + List.fold_left + (function metasenv -> aux metasenv k) metasenv'' pl + | C.Fix (i, fl) -> + let len = List.length fl in + List.fold_left + (fun metasenv f -> + let (_,_,ty,bo) = f in + let metasenv' = aux metasenv k ty in + aux metasenv' (k+len) bo + ) metasenv fl + | C.CoFix (i, fl) -> + let len = List.length fl in + List.fold_left + (fun metasenv f -> + let (_,ty,bo) = f in + let metasenv' = aux metasenv k ty in + aux metasenv' (k+len) bo + ) metasenv fl + in aux metasenv 0 +;; +*) + + +let unwind metasenv subst unwinded t = let unwinded = ref unwinded in let frozen = ref [] in - let rec um_aux k = + let rec um_aux metasenv = let module C = Cic in let module S = CicSubstitution in function - C.Rel _ as t -> t - | C.Var _ as t -> t - | C.Meta i as t ->(try S.lift k (List.assoc i !unwinded) - with Not_found -> - if List.mem i !frozen then - raise OccurCheck - else - let saved_frozen = !frozen in - frozen := i::!frozen ; - let res = - try - let t = List.assoc i subst in - let t' = um_aux 0 t in - unwinded := (i,t')::!unwinded ; - S.lift k t' - with - Not_found -> - (* not constrained variable, i.e. free in subst*) - C.Meta i - in - frozen := saved_frozen ; - res - ) - | C.Sort _ as t -> t - | C.Implicit as t -> t - | C.Cast (te,ty) -> C.Cast (um_aux k te, um_aux k ty) - | C.Prod (n,s,t) -> C.Prod (n, um_aux k s, um_aux (k+1) t) - | C.Lambda (n,s,t) -> C.Lambda (n, um_aux k s, um_aux (k+1) t) - | C.LetIn (n,s,t) -> C.LetIn (n, um_aux k s, um_aux (k+1) t) + C.Rel _ as t -> t,metasenv + | C.Var _ as t -> t,metasenv + | C.Meta (i,l) -> + (try + S.lift_meta l (List.assoc i !unwinded), metasenv + with Not_found -> + if List.mem i !frozen then raise OccurCheck + else + let saved_frozen = !frozen in + frozen := i::!frozen ; + let res = + try + let t = List.assoc i subst in + let t',metasenv' = um_aux metasenv t in + let _,metasenv'' = + let (_,canonical_context,_) = + List.find (function (m,_,_) -> m=i) metasenv + in +prerr_endline ("DELIFT(" ^ CicPp.ppterm t' ^ ")") ; flush stderr ; +List.iter (function (Some t) -> prerr_endline ("l: " ^ CicPp.ppterm t) | None -> prerr_endline " _ ") l ; flush stderr ; +prerr_endline " + (* not constrained variable, i.e. free in subst*) + let l',metasenv' = + List.fold_right + (fun t (tl,metasenv) -> + match t with + None -> None::tl,metasenv + | Some t -> + let t',metasenv' = um_aux metasenv t in + (Some t')::tl, metasenv' + ) l ([],metasenv) + in + C.Meta (i,l'), metasenv' + in + frozen := saved_frozen ; + res + ) + | C.Sort _ + | C.Implicit as t -> t,metasenv + | C.Cast (te,ty) -> + let te',metasenv' = um_aux metasenv te in + let ty',metasenv'' = um_aux metasenv' ty in + C.Cast (te',ty'),metasenv'' + | C.Prod (n,s,t) -> + let s',metasenv' = um_aux metasenv s in + let t',metasenv'' = um_aux metasenv' t in + C.Prod (n, s', t'), metasenv'' + | C.Lambda (n,s,t) -> + let s',metasenv' = um_aux metasenv s in + let t',metasenv'' = um_aux metasenv' t in + C.Lambda (n, s', t'), metasenv'' + | C.LetIn (n,s,t) -> + let s',metasenv' = um_aux metasenv s in + let t',metasenv'' = um_aux metasenv' t in + C.LetIn (n, s', t'), metasenv'' | C.Appl (he::tl) -> - let tl' = List.map (um_aux k) tl in + let tl',metasenv' = + List.fold_right + (fun t (tl,metasenv) -> + let t',metasenv' = um_aux metasenv t in + t'::tl, metasenv' + ) tl ([],metasenv) + in begin - match um_aux k he with - C.Appl l -> C.Appl (l@tl') - | _ as he' -> C.Appl (he'::tl') + match um_aux metasenv' he with + (C.Appl l, metasenv'') -> C.Appl (l@tl'),metasenv'' + | (he', metasenv'') -> C.Appl (he'::tl'),metasenv'' end | C.Appl _ -> assert false - | C.Const _ as t -> t - | C.Abst _ as t -> t - | C.MutInd _ as t -> t - | C.MutConstruct _ as t -> t + | C.Const _ + | C.Abst _ + | C.MutInd _ + | C.MutConstruct _ as t -> t,metasenv | C.MutCase (sp,cookingsno,i,outty,t,pl) -> - C.MutCase (sp, cookingsno, i, um_aux k outty, um_aux k t, - List.map (um_aux k) pl) + let outty',metasenv' = um_aux metasenv outty in + let t',metasenv'' = um_aux metasenv' t in + let pl',metasenv''' = + List.fold_right + (fun p (pl,metasenv) -> + let p',metasenv' = um_aux metasenv p in + p'::pl, metasenv' + ) pl ([],metasenv'') + in + C.MutCase (sp, cookingsno, i, outty', t', pl'),metasenv''' | C.Fix (i, fl) -> let len = List.length fl in - let liftedfl = - List.map - (fun (name, i, ty, bo) -> (name, i, um_aux k ty, um_aux (k+len) bo)) - fl + let liftedfl,metasenv' = + List.fold_right + (fun (name, i, ty, bo) (fl,metasenv) -> + let ty',metasenv' = um_aux metasenv ty in + let bo',metasenv'' = um_aux metasenv' bo in + (name, i, ty', bo')::fl,metasenv'' + ) fl ([],metasenv) in - C.Fix (i, liftedfl) + C.Fix (i, liftedfl),metasenv' | C.CoFix (i, fl) -> let len = List.length fl in - let liftedfl = - List.map - (fun (name, ty, bo) -> (name, um_aux k ty, um_aux (k+len) bo)) - fl + let liftedfl,metasenv' = + List.fold_right + (fun (name, ty, bo) (fl,metasenv) -> + let ty',metasenv' = um_aux metasenv ty in + let bo',metasenv'' = um_aux metasenv' bo in + (name, ty', bo')::fl,metasenv'' + ) fl ([],metasenv) in - C.CoFix (i, liftedfl) + C.CoFix (i, liftedfl),metasenv' in - um_aux 0 t,!unwinded + let t',metasenv' = um_aux metasenv t in + t',metasenv',!unwinded ;; (* apply_subst_reducing subst (Some (mtr,reductions_no)) t *) @@ -265,33 +395,33 @@ let unwind subst unwinded t = let apply_subst_reducing subst meta_to_reduce t = let unwinded = ref subst in - let rec um_aux k = + let rec um_aux = let module C = Cic in let module S = CicSubstitution in function - C.Rel _ as t -> t + C.Rel _ | C.Var _ as t -> t - | C.Meta i as t -> + | C.Meta (i,l) as t -> (try - S.lift k (List.assoc i !unwinded) + S.lift_meta l (List.assoc i !unwinded) with Not_found -> - C.Meta i) + C.Meta (i,l)) | C.Sort _ as t -> t | C.Implicit as t -> t - | C.Cast (te,ty) -> C.Cast (um_aux k te, um_aux k ty) - | C.Prod (n,s,t) -> C.Prod (n, um_aux k s, um_aux (k+1) t) - | C.Lambda (n,s,t) -> C.Lambda (n, um_aux k s, um_aux (k+1) t) - | C.LetIn (n,s,t) -> C.LetIn (n, um_aux k s, um_aux (k+1) t) + | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty) + | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t) + | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t) + | C.LetIn (n,s,t) -> C.LetIn (n, um_aux s, um_aux t) | C.Appl (he::tl) -> - let tl' = List.map (um_aux k) tl in + let tl' = List.map um_aux tl in let t' = - match um_aux k he with + match um_aux he with C.Appl l -> C.Appl (l@tl') | _ as he' -> C.Appl (he'::tl') in begin - match meta_to_reduce with - Some (mtr,reductions_no) when he = C.Meta mtr -> + match meta_to_reduce,he with + Some (mtr,reductions_no), C.Meta (m,_) when m = mtr -> let rec beta_reduce = function (n,(C.Appl (C.Lambda (_,_,t)::he'::tl'))) when n > 0 -> @@ -303,7 +433,7 @@ let apply_subst_reducing subst meta_to_reduce t = | (_,t) -> t in beta_reduce (reductions_no,t') - | _ -> t' + | _,_ -> t' end | C.Appl _ -> assert false | C.Const _ as t -> t @@ -311,13 +441,13 @@ let apply_subst_reducing subst meta_to_reduce t = | C.MutInd _ as t -> t | C.MutConstruct _ as t -> t | C.MutCase (sp,cookingsno,i,outty,t,pl) -> - C.MutCase (sp, cookingsno, i, um_aux k outty, um_aux k t, - List.map (um_aux k) pl) + C.MutCase (sp, cookingsno, i, um_aux outty, um_aux t, + List.map um_aux pl) | C.Fix (i, fl) -> let len = List.length fl in let liftedfl = List.map - (fun (name, i, ty, bo) -> (name, i, um_aux k ty, um_aux (k+len) bo)) + (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo)) fl in C.Fix (i, liftedfl) @@ -325,32 +455,60 @@ let apply_subst_reducing subst meta_to_reduce t = let len = List.length fl in let liftedfl = List.map - (fun (name, ty, bo) -> (name, um_aux k ty, um_aux (k+len) bo)) + (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo)) fl in C.CoFix (i, liftedfl) in - um_aux 0 t + um_aux t ;; (* UNWIND THE MGU INSIDE THE MGU *) -let unwind_subst subst = +let unwind_subst metasenv subst = + let identity_relocation_list_for_metavariable i = + let (_,canonical_context,_) = + List.find (function (m,_,_) -> m=i) metasenv + in + let canonical_context_length = List.length canonical_context in + let rec aux = + function + n when n > canonical_context_length -> [] + | n -> (Some (Cic.Rel n))::(aux (n+1)) + in + aux 1 + in List.fold_left - (fun unwinded (i,_) -> snd (unwind subst unwinded (Cic.Meta i))) [] subst + (fun (unwinded,metasenv) (i,_) -> + let identity_relocation_list = + identity_relocation_list_for_metavariable i + in + let (_,metasenv',subst') = + unwind metasenv subst unwinded (Cic.Meta (i,identity_relocation_list)) + in + subst',metasenv' + ) ([],metasenv) subst ;; let apply_subst subst t = - fst (unwind [] subst t) + (* metasenv will not be used nor modified. So, let's use a dummy empty one *) + let metasenv = [] in + let (t',_,_) = unwind metasenv [] subst t in + t' ;; -(* A substitution is a (int * Cic.term) list that associates a - metavariable i with its body. - A metaenv is a (int * Cic.term) list that associate a metavariable - i with is type. - fo_unif takes a metasenv, a context, - two terms t1 and t2 and gives back a new - substitution which is already unwinded and ready to be applied. *) +(* A substitution is a (int * Cic.term) list that associates a *) +(* metavariable i with its body. *) +(* metasenv is of type Cic.metasenv *) +(* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *) +(* 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 = - let subst_to_unwind = fo_unif_new metasenv context t1 t2 in - unwind_subst subst_to_unwind +prerr_endline "INIZIO FASE 1" ; flush stderr ; + let subst_to_unwind,metasenv' = fo_unif_new metasenv context t1 t2 in +prerr_endline "FINE FASE 1" ; flush stderr ; +let res = + unwind_subst metasenv' subst_to_unwind +in +prerr_endline "FINE FASE 2" ; flush stderr ; res ;; diff --git a/helm/ocaml/cic_unification/cicUnification.mli b/helm/ocaml/cic_unification/cicUnification.mli index 9fde49d9e..2ec49722e 100644 --- a/helm/ocaml/cic_unification/cicUnification.mli +++ b/helm/ocaml/cic_unification/cicUnification.mli @@ -36,7 +36,8 @@ type substitution = (int * Cic.term) list (* Only the metavariables declared in [metasenv] *) (* can be used in [t1] and [t2]. *) val fo_unif : - (int * Cic.term) list -> Cic.context -> Cic.term -> Cic.term -> substitution + Cic.metasenv -> Cic.context -> Cic.term -> Cic.term -> + substitution * Cic.metasenv (* apply_subst subst t *) (* applies the substitution [sust] to [t] *) -- 2.39.2