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 *)
| 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 *)
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 *)
| 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 , *)
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;;
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"] *)
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
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 =
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
| _ -> 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)
;;
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
;;
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)
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) ->
;;
(*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
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 >]
| 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
>]
end
>]
;;
+
+
+
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
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)
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,_,_) ->
*.cm[iaox] *.cmxa
+cicReduction.ml
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
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"
| 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
"\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 ^
"}\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 ^
(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
) 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 ""
;;
(* 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
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 ??? *)
+
+
+
+
exception ReferenceToVariable;;
exception ReferenceToCurrentProof;;
exception ReferenceToInductiveDefinition;;
+exception RelToHiddenHypothesis;;
(* takes a well-typed term *)
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
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
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 ->
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 ->
* http://cs.unibo.it/helm/.
*)
+exception CannotSubstInMeta;;
+exception RelToHiddenHypothesis;;
+
let lift n =
let rec liftaux k =
let module C = Cic in
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)
| _ -> 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)
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
+;;
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
exception NotPositiveOccurrences of string;;
exception NotWellFormedTypeOfInductiveConstructor of string;;
exception WrongRequiredArgument of string;;
+exception RelToHiddenHypothesis;;
+exception MetasenvInconsistency;;
let fdebug = ref 0;;
let debug t context =
| 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 _
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 &&
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 &&
| 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 *)
| 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
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
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! *)
(*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 ->
| 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 _ -> []
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' =
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, [])
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 =
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)
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 *)
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
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) ->
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 ->
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 ->
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 _
| 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
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) ->
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) ->
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 ->
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 ->
| 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
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
| 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 *)
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 &&
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 &&
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 &&
| (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
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
)
| _ -> 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
| _ ->
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 =
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")
)
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
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
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
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
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 ->
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!!! *)
| _ -> 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) ->
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
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
(* 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
| '?' { IMPLICIT }
| '(' { LPAREN }
| ')' { RPAREN }
+ | '[' { LBRACKET }
+ | ']' { RBRACKET }
| '{' { LCURLY }
| '}' { RCURLY }
| ';' { SEMICOLON }
| ':' { COLON }
| '.' { DOT }
| "->" { ARROW }
+ | "_" { NONE }
| eof { EOF }
{}
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
%token <UriManager.uri * int> INDTYURI
%token <UriManager.uri * int * int> 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 <Cic.term option> main
| 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 :
;
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
}
;
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
}
;
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:
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
Hashtbl.add uri_of_id_map $2
(Cic.MutConstruct (uri, cookingno, indno ,consno))
}
+
+
+
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);;
*)
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
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<m
- then (m, C.Meta n)::subst
- else (n, C.Meta m)::subst
- | (C.Meta n, tm) -> (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 "<DELIFT2" ; flush stderr ;
+ let t',metasenv' = S.delift context metasenv l t in
+ (n, t')::subst, metasenv'
+ in
+ let (_,_,meta_type) =
+ List.find (function (m,_,_) -> 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 _, _)
| (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 _, _)
| (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 "<DELIFT" ; flush stderr ;
+ S.delift canonical_context metasenv' l t'
+ in
+ unwinded := (i,t')::!unwinded ;
+ S.lift_meta l t', metasenv'
+ with
+ Not_found ->
+ (* 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 *)
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 ->
| (_,t) -> t
in
beta_reduce (reductions_no,t')
- | _ -> t'
+ | _,_ -> t'
end
| C.Appl _ -> assert false
| C.Const _ 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, 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)
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
;;
(* 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] *)
projects / helm.git / commitdiff