| 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.LetIn (n,s,ty,t) -> C.LetIn (n, um_aux s, um_aux ty, um_aux t)
| C.Appl (hd :: tl) -> appl_fun um_aux hd tl
| C.Appl _ -> assert false
| C.Const (uri,exp_named_subst) ->
let t' = apply_subst subst t in
Some (n, Cic.Decl t') :: context
| Some (n, Cic.Def (t, ty)) ->
- let ty' =
- match ty with
- | None -> None
- | Some ty -> Some (apply_subst subst ty)
- in
+ let ty' = apply_subst subst ty in
let t' = apply_subst subst t in
Some (n, Cic.Def (t', ty')) :: context
| None -> None :: context)
let ppterm ~metasenv subst term =
CicPp.ppterm ~metasenv (apply_subst subst term)
-let ppterm_in_name_context ~metasenv subst term name_context =
- CicPp.pp ~metasenv (apply_subst subst term) name_context
-
let ppterm_in_context ~metasenv subst term context =
let name_context =
List.map (function None -> None | Some (n,_) -> Some n) context
in
- ppterm_in_name_context ~metasenv subst term name_context
+ CicPp.pp ~metasenv (apply_subst subst term) name_context
let ppterm_in_context_ref = ref ppterm_in_context
let set_ppterm_in_context f =
let ppcontext' ~metasenv ?(sep = "\n") subst context =
let separate s = if s = "" then "" else s ^ sep in
List.fold_right
- (fun context_entry (i,name_context) ->
+ (fun context_entry (i,context) ->
match context_entry with
Some (n,Cic.Decl t) ->
sprintf "%s%s : %s" (separate i) (CicPp.ppname n)
- (ppterm_in_name_context ~metasenv subst t name_context),
- (Some n)::name_context
+ (ppterm_in_context ~metasenv subst t context),
+ context_entry::context
| Some (n,Cic.Def (bo,ty)) ->
sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n)
- (match ty with
- None -> "_"
- | Some ty -> ppterm_in_name_context ~metasenv subst ty name_context)
- (ppterm_in_name_context ~metasenv subst bo name_context), (Some n)::name_context
+ (ppterm_in_context ~metasenv subst ty context)
+ (ppterm_in_context ~metasenv subst bo context),
+ context_entry::context
| None ->
- sprintf "%s_ :? _" (separate i), None::name_context
+ sprintf "%s_ :? _" (separate i), context_entry::context
) context ("",[])
let ppsubst_unfolded ~metasenv subst =
String.concat "\n"
(List.map
(fun (idx, (c, t,ty)) ->
- let context,name_context = ppcontext' ~metasenv ~sep:"; " subst c in
- sprintf "%s |- ?%d : %s := %s" context idx
-(ppterm_in_name_context ~metasenv [] ty name_context)
- (ppterm_in_name_context ~metasenv subst t name_context))
+ let scontext,context = ppcontext' ~metasenv ~sep:"; " subst c in
+ sprintf "%s |- ?%d : %s := %s" scontext idx
+(ppterm_in_context ~metasenv [] ty context)
+ (ppterm_in_context ~metasenv subst t context))
subst)
(*
Printf.sprintf "?%d := %s" idx (CicPp.ppterm term))
String.concat "\n"
(List.map
(fun (idx, (c, t, ty)) ->
- let context,name_context = ppcontext' ~metasenv ~sep:"; " [] c in
- sprintf "%s |- ?%d : %s := %s" context idx (ppterm_in_name_context ~metasenv [] ty name_context)
- (ppterm_in_name_context ~metasenv [] t name_context))
+ let scontext,context = ppcontext' ~metasenv ~sep:"; " [] c in
+ sprintf "%s |- ?%d : %s := %s" scontext idx (ppterm_in_context ~metasenv [] ty context)
+ (ppterm_in_context ~metasenv [] t context))
subst)
;;
String.concat sep
(List.map
(fun (i, c, t) ->
- let context,name_context = ppcontext' ~metasenv ~sep:"; " subst c in
- sprintf "%s |- ?%d: %s" context i
- (ppterm_in_name_context ~metasenv subst t name_context))
+ let scontext,context = ppcontext' ~metasenv ~sep:"; " subst c in
+ sprintf "%s |- ?%d: %s" scontext i
+ (ppterm_in_context ~metasenv subst t context))
(List.filter
(fun (i, _, _) -> not (List.mem_assoc i subst))
metasenv))
| C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
| C.Prod (name,so,dest) -> C.Prod (name, aux k so, aux (k+1) dest)
| C.Lambda (name,so,dest) -> C.Lambda (name, aux k so, aux (k+1) dest)
- | C.LetIn (name,so,dest) -> C.LetIn (name, aux k so, aux (k+1) dest)
+ | C.LetIn (name,so,ty,dest) ->
+ C.LetIn (name, aux k so, aux k ty, aux (k+1) dest)
| C.Appl l -> C.Appl (List.map (aux k) l)
| C.Var (uri,exp_named_subst) ->
let exp_named_subst' =
force_does_not_occur subst to_be_restricted bo
in
let more_to_be_restricted, ty' =
- match ty with
- | None -> more_to_be_restricted, None
- | Some ty ->
- let more_to_be_restricted', ty' =
- force_does_not_occur subst to_be_restricted ty
- in
- more_to_be_restricted @ more_to_be_restricted',
- Some ty'
+ let more_to_be_restricted', ty' =
+ force_does_not_occur subst to_be_restricted ty
+ in
+ more_to_be_restricted @ more_to_be_restricted',
+ ty'
in
more_to_be_restricted, Some (name, Cic.Def (bo', ty'))
in
let module S = CicSubstitution in
let l =
- let (_, canonical_context, _) = CicUtil.lookup_meta n metasenv in
+ let (_, canonical_context, _) =
+ try
+ CicUtil.lookup_meta n metasenv
+ with CicUtil.Meta_not_found _ ->
+ raise (MetaSubstFailure (lazy
+ ("delifting error: the metavariable " ^ string_of_int n ^ " is not " ^
+ "declared in the metasenv")))
+ in
List.map2 (fun ct lt ->
match (ct, lt) with
| None, _ -> None
(try
match List.nth context (m-k-1) with
Some (_,C.Def (t,_)) ->
+ (try
+ C.Rel ((position (m-k) l) + k)
+ with
+ NotInTheList ->
(*CSC: Hmmm. This bit of reduction is not in the spirit of *)
(*CSC: first order unification. Does it help or does it harm? *)
(*CSC: ANSWER: it hurts performances since it is possible to *)
(*CSC: have an exponential explosion of the size of the proof.*)
(*CSC: However, without this bit of reduction some "apply" in *)
(*CSC: the library fail (e.g. nat/nth_prime.ma). *)
- deliftaux k (S.lift m t)
+ deliftaux k (S.lift m t))
| Some (_,C.Decl t) ->
C.Rel ((position (m-k) l) + k)
| None -> raise (MetaSubstFailure (lazy "RelToHiddenHypothesis"))
| 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.LetIn (n,s,ty,t) ->
+ C.LetIn (n, deliftaux k s, deliftaux k ty, deliftaux (k+1) t)
| C.Appl l -> C.Appl (List.map (deliftaux k) l)
| C.Const (uri,exp_named_subst) ->
let exp_named_subst' =
let s',subst,metasenv = liftaux subst metasenv k s in
let t',subst,metasenv = liftaux subst metasenv (k+1) t in
C.Lambda (n,s',t'),subst,metasenv
- | C.LetIn (n,s,t) ->
+ | C.LetIn (n,s,ty,t) ->
let s',subst,metasenv = liftaux subst metasenv k s in
+ let ty',subst,metasenv = liftaux subst metasenv k ty in
let t',subst,metasenv = liftaux subst metasenv (k+1) t in
- C.LetIn (n,s',t'),subst,metasenv
+ C.LetIn (n,s',ty',t'),subst,metasenv
| C.Appl l ->
let l',subst,metasenv =
List.fold_right
projects / helm.git / blobdiff