| (_,_) -> raise (AssertFailure "split: list too short")
;;
+let look_for_coercion src tgt =
+ if (src = (CicUtil.term_of_uri "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)")) &&
+ (tgt = (CicUtil.term_of_uri "cic:/Coq/Reals/Rdefinitions/R.con"))
+ then
+ begin
+ prerr_endline "TROVATA coercion";
+ Some (CicUtil.term_of_uri "cic://Coq/Reals/Raxioms/INR.con")
+ end
+ else
+ begin
+ prerr_endline (sprintf "NON TROVATA la coercion %s %s" (CicPp.ppterm src)
+ (CicPp.ppterm tgt));
+ None
+ end
+;;
+
+
let rec type_of_constant uri ugraph =
let module C = Cic in
let module R = CicReduction in
C.Rel n ->
(try
match List.nth context (n - 1) with
- Some (_,C.Decl t) -> S.lift n t,subst,metasenv, ugraph
- | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv, ugraph
+ Some (_,C.Decl ty) ->
+ t,S.lift n ty,subst,metasenv, ugraph
+ | Some (_,C.Def (_,Some ty)) ->
+ t,S.lift n ty,subst,metasenv, ugraph
| Some (_,C.Def (bo,None)) ->
type_of_aux subst metasenv context (S.lift n bo) ugraph
| None -> raise (RefineFailure "Rel to hidden hypothesis")
_ -> raise (RefineFailure "Not a close term")
)
| C.Var (uri,exp_named_subst) ->
- let subst',metasenv',ugraph1 =
- check_exp_named_subst subst metasenv context exp_named_subst ugraph in
- let ty_uri,ugraph1 = type_of_variable uri ugraph in
-
+ let exp_named_subst',subst',metasenv',ugraph1 =
+ check_exp_named_subst
+ subst metasenv context exp_named_subst ugraph
+ in
+ let ty_uri,ugraph1 = type_of_variable uri ugraph in
let ty =
- CicSubstitution.subst_vars exp_named_subst ty_uri
+ CicSubstitution.subst_vars exp_named_subst' ty_uri
in
- ty,subst',metasenv',ugraph1
+ C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
| C.Meta (n,l) ->
(try
- let (canonical_context, term,ty) = CicUtil.lookup_subst n subst in
- let subst,metasenv,ugraph1 =
+ let (canonical_context, term,ty) =
+ CicUtil.lookup_subst n subst
+ in
+ let l',subst',metasenv',ugraph1 =
check_metasenv_consistency n subst metasenv context
canonical_context l ugraph
in
(* trust or check ??? *)
- CicSubstitution.lift_meta l ty, subst, metasenv, ugraph1
+ C.Meta (n,l'),CicSubstitution.lift_meta l' ty,
+ subst', metasenv', ugraph1
(* type_of_aux subst metasenv
context (CicSubstitution.lift_meta l term) *)
with CicUtil.Subst_not_found _ ->
let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
- let subst,metasenv, ugraph1 =
+ let l',subst',metasenv', ugraph1 =
check_metasenv_consistency n subst metasenv context
canonical_context l ugraph
in
- CicSubstitution.lift_meta l ty, subst, metasenv,ugraph1)
- (* TASSI: CONSTRAINT *)
- | C.Sort (C.Type t) ->
- let t' = CicUniv.fresh() in
- let ugraph1 = CicUniv.add_gt t' t ugraph in
- (C.Sort (C.Type t')),subst,metasenv,ugraph1
- (* TASSI: CONSTRAINT *)
- | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
+ C.Meta (n,l'),CicSubstitution.lift_meta l' ty,
+ subst', metasenv',ugraph1)
+ | C.Sort (C.Type tno) ->
+ let tno' = CicUniv.fresh() in
+ let ugraph1 = CicUniv.add_gt tno' tno ugraph in
+ t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
+ | C.Sort _ ->
+ t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
| C.Implicit _ -> raise (AssertFailure "21")
| C.Cast (te,ty) ->
- let _,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context ty ugraph in
- let inferredty,subst'',metasenv'',ugraph2 =
+ let ty',_,subst',metasenv',ugraph1 =
+ type_of_aux subst metasenv context ty ugraph
+ in
+ let te',inferredty,subst'',metasenv'',ugraph2 =
type_of_aux subst' metasenv' context te ugraph1
in
(try
let subst''',metasenv''',ugraph3 =
- fo_unif_subst subst'' context metasenv'' inferredty ty ugraph2
+ fo_unif_subst subst'' context metasenv''
+ inferredty ty' ugraph2
in
- ty,subst''',metasenv''',ugraph3
+ C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
with
_ -> raise (RefineFailure "Cast"))
| C.Prod (name,s,t) ->
- let sort1,subst',metasenv',ugraph1 = type_of_aux subst metasenv context s ugraph in
- let sort2,subst'',metasenv'',ugraph2 =
- type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t ugraph1
+ let s',sort1,subst',metasenv',ugraph1 =
+ type_of_aux subst metasenv context s ugraph
+ in
+ let t',sort2,subst'',metasenv'',ugraph2 =
+ type_of_aux subst' metasenv'
+ ((Some (name,(C.Decl s')))::context) t ugraph1
in
- sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2) ugraph2
+ let sop,subst''',metasenv''',ugraph3 =
+ sort_of_prod subst'' metasenv''
+ context (name,s') (sort1,sort2) ugraph2
+ in
+ C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
| C.Lambda (n,s,t) ->
- let sort1,subst',metasenv',ugraph1 =
+ let s',sort1,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context s ugraph
in
(match CicReduction.whd ~subst:subst' context sort1 with
instead it is a term of type %s" (CicPp.ppterm s)
(CicPp.ppterm sort1)))
) ;
- let type2,subst'',metasenv'',ugraph2 =
- type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t ugraph1
+ let t',type2,subst'',metasenv'',ugraph2 =
+ type_of_aux subst' metasenv'
+ ((Some (n,(C.Decl s')))::context) t ugraph1
in
- C.Prod (n,s,type2),subst'',metasenv'',ugraph2
+ C.Lambda (n,s',t'),C.Prod (n,s',type2),
+ subst'',metasenv'',ugraph2
| C.LetIn (n,s,t) ->
(* only to check if s is well-typed *)
- let ty,subst',metasenv',ugraph1 =
+ let s',ty,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context s ugraph
in
- let inferredty,subst'',metasenv'',ugraph2 =
- type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t ugraph1
+ let t',inferredty,subst'',metasenv'',ugraph2 =
+ type_of_aux subst' metasenv'
+ ((Some (n,(C.Def (s',Some ty))))::context) t ugraph1
in
- (* One-step LetIn reduction. Even faster than the previous solution.
- Moreover the inferred type is closer to the expected one. *)
- CicSubstitution.subst s inferredty,subst',metasenv',ugraph2
+ (* One-step LetIn reduction.
+ * Even faster than the previous solution.
+ * Moreover the inferred type is closer to the expected one.
+ *)
+ C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
+ subst',metasenv',ugraph2
| C.Appl (he::((_::_) as tl)) ->
- let hetype,subst',metasenv',ugraph1 =
+ let he',hetype,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context he ugraph
in
let tlbody_and_type,subst'',metasenv'',ugraph2 =
List.fold_right
(fun x (res,subst,metasenv,ugraph) ->
- let ty,subst',metasenv',ugraph1 =
+ let x',ty,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context x ugraph
in
- (x, ty)::res,subst',metasenv',ugraph1
+ (x', ty)::res,subst',metasenv',ugraph1
) tl ([],subst',metasenv',ugraph1)
in
- eat_prods subst'' metasenv'' context hetype tlbody_and_type ugraph2
+ let tl',applty,subst''',metasenv''',ugraph3 =
+ eat_prods subst'' metasenv'' context
+ hetype tlbody_and_type ugraph2
+ in
+ C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
| C.Appl _ -> raise (RefineFailure "Appl: no arguments")
| C.Const (uri,exp_named_subst) ->
- let subst',metasenv',ugraph1 =
- check_exp_named_subst subst metasenv context exp_named_subst ugraph in
+ let exp_named_subst',subst',metasenv',ugraph1 =
+ check_exp_named_subst subst metasenv context
+ exp_named_subst ugraph in
let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
let cty =
- CicSubstitution.subst_vars exp_named_subst ty_uri
+ CicSubstitution.subst_vars exp_named_subst' ty_uri
in
- cty,subst',metasenv',ugraph2
+ C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
| C.MutInd (uri,i,exp_named_subst) ->
- let subst',metasenv',ugraph1 =
- check_exp_named_subst subst metasenv context exp_named_subst ugraph
+ let exp_named_subst',subst',metasenv',ugraph1 =
+ check_exp_named_subst subst metasenv context
+ exp_named_subst ugraph
in
let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
let cty =
- CicSubstitution.subst_vars exp_named_subst ty_uri in
- cty,subst',metasenv',ugraph2
+ CicSubstitution.subst_vars exp_named_subst' ty_uri in
+ C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
| C.MutConstruct (uri,i,j,exp_named_subst) ->
- let subst',metasenv',ugraph1 =
- check_exp_named_subst subst metasenv context exp_named_subst ugraph in
- let ty_uri,ugraph2 = type_of_mutual_inductive_constr uri i j ugraph1 in
+ let exp_named_subst',subst',metasenv',ugraph1 =
+ check_exp_named_subst subst metasenv context
+ exp_named_subst ugraph
+ in
+ let ty_uri,ugraph2 =
+ type_of_mutual_inductive_constr uri i j ugraph1
+ in
let cty =
- CicSubstitution.subst_vars exp_named_subst ty_uri in
- cty,subst',metasenv',ugraph2
+ CicSubstitution.subst_vars exp_named_subst' ty_uri
+ in
+ C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
+ metasenv',ugraph2
| C.MutCase (uri, i, outtype, term, pl) ->
- (* first, get the inductive type (and noparams) in the environment *)
+ (* first, get the inductive type (and noparams)
+ * in the environment *)
let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
(*
let obj =
| _ ->
raise
(RefineFailure
- ("Unkown mutual inductive definition " ^ U.string_of_uri uri)) in
+ ("Unkown mutual inductive definition " ^
+ U.string_of_uri uri))
+ in
let rec count_prod t =
match CicReduction.whd ~subst context t with
C.Prod (_, _, t) -> 1 + (count_prod t)
- | _ -> 0 in
+ | _ -> 0
+ in
let no_args = count_prod arity in
(* now, create a "generic" MutInd *)
let metasenv,left_args =
- CicMkImplicit.n_fresh_metas metasenv subst context no_left_params in
+ CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
+ in
let metasenv,right_args =
let no_right_params = no_args - no_left_params in
if no_right_params < 0 then assert false
- else CicMkImplicit.n_fresh_metas metasenv subst context no_right_params in
+ else CicMkImplicit.n_fresh_metas
+ metasenv subst context no_right_params
+ in
let metasenv,exp_named_subst =
CicMkImplicit.fresh_subst metasenv subst context expl_params in
let expected_type =
if no_args = 0 then
C.MutInd (uri,i,exp_named_subst)
else
- C.Appl (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
+ C.Appl
+ (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
in
(* check consistency with the actual type of term *)
- let actual_type,subst,metasenv,ugraph1 =
+ let term',actual_type,subst,metasenv,ugraph1 =
type_of_aux subst metasenv context term ugraph in
- let _, subst, metasenv,ugraph2 =
+ let expected_type',_, subst, metasenv,ugraph2 =
type_of_aux subst metasenv context expected_type ugraph1
in
let actual_type = CicReduction.whd ~subst context actual_type in
let subst,metasenv,ugraph3 =
- fo_unif_subst subst context metasenv expected_type actual_type ugraph2
+ fo_unif_subst subst context metasenv
+ expected_type' actual_type ugraph2
in
- (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
- let (_,outtypeinstances,subst,metasenv,ugraph4) =
+ (* TODO: check if the sort elimination
+ * is allowed: [(I q1 ... qr)|B] *)
+ let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
List.fold_left
- (fun (j,outtypeinstances,subst,metasenv,ugraph) p ->
+ (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
let constructor =
if left_args = [] then
(C.MutConstruct (uri,i,j,exp_named_subst))
else
(C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
in
- let actual_type,subst,metasenv,ugraph1 =
- type_of_aux subst metasenv context p ugraph in
- let expected_type, subst, metasenv,ugraph2 =
- type_of_aux subst metasenv context constructor ugraph1 in
+ let p',actual_type,subst,metasenv,ugraph1 =
+ type_of_aux subst metasenv context p ugraph
+ in
+ let constructor',expected_type, subst, metasenv,ugraph2 =
+ type_of_aux subst metasenv context constructor ugraph1
+ in
let outtypeinstance,subst,metasenv,ugraph3 =
- check_branch
- 0 context metasenv subst
- no_left_params actual_type constructor expected_type ugraph2 in
- (j+1,outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
- (1,[],subst,metasenv,ugraph3) pl in
+ check_branch 0 context metasenv subst no_left_params
+ actual_type constructor expected_type ugraph2
+ in
+ (pl @ [p'],j+1,
+ outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
+ ([],1,[],subst,metasenv,ugraph3) pl
+ in
(* we are left to check that the outype matches his instances.
The easy case is when the outype is specified, that amount
to a trivial check. Otherwise, we should guess a type from
its instances *)
(* easy case *)
- let _, subst, metasenv,ugraph5 =
+ let _,_, subst, metasenv,ugraph5 =
type_of_aux subst metasenv context
- (C.Appl ((outtype :: right_args) @ [term])) ugraph4
+ (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
in
let (subst,metasenv,ugraph6) =
List.fold_left
(* CicMetaSubst.whd subst context appl *)
CicReduction.whd ~subst context appl
in
- fo_unif_subst subst context metasenv instance instance' ugraph)
- (subst,metasenv,ugraph5) outtypeinstances in
- CicReduction.whd ~subst
- context (C.Appl(outtype::right_args@[term])),subst,metasenv,ugraph6
+ fo_unif_subst subst context metasenv
+ instance instance' ugraph)
+ (subst,metasenv,ugraph5) outtypeinstances
+ in
+ C.MutCase (uri, i, outtype, term', pl'),
+ CicReduction.whd ~subst context
+ (C.Appl(outtype::right_args@[term])),
+ subst,metasenv,ugraph6
| C.Fix (i,fl) ->
- let subst,metasenv,types,ugraph1 =
+ let fl_ty',subst,metasenv,types,ugraph1 =
List.fold_left
- (fun (subst,metasenv,types,ugraph) (n,_,ty,_) ->
- let _,subst',metasenv',ugraph1 = type_of_aux subst metasenv context ty ugraph in
- subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types, ugraph
- ) (subst,metasenv,[],ugraph) fl
+ (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
+ let ty',_,subst',metasenv',ugraph1 =
+ type_of_aux subst metasenv context ty ugraph
+ in
+ fl @ [ty'],subst',metasenv',
+ Some (C.Name n,(C.Decl ty')) :: types, ugraph
+ ) ([],subst,metasenv,[],ugraph) fl
in
let len = List.length types in
let context' = types@context in
- let subst,metasenv,ugraph2 =
+ let fl_bo',subst,metasenv,ugraph2 =
List.fold_left
- (fun (subst,metasenv,ugraph) (name,x,ty,bo) ->
- let ty_of_bo,subst,metasenv,ugraph1 =
+ (fun (fl,subst,metasenv,ugraph) (name,x,ty,bo) ->
+ let bo',ty_of_bo,subst,metasenv,ugraph1 =
type_of_aux subst metasenv context' bo ugraph
in
+ let subst',metasenv',ugraph' =
fo_unif_subst subst context' metasenv
ty_of_bo (CicSubstitution.lift len ty) ugraph1
- ) (subst,metasenv,ugraph1) fl in
+ in
+ fl @ [bo'] , subst',metasenv',ugraph'
+ ) ([],subst,metasenv,ugraph1) fl
+ in
let (_,_,ty,_) = List.nth fl i in
- ty,subst,metasenv,ugraph2
+ (* now we have the new ty in fl_ty', the new bo in fl_bo',
+ * and we want the new fl with bo' and ty' injected in the right
+ * place.
+ *)
+ let rec map3 f l1 l2 l3 =
+ match l1,l2,l3 with
+ | [],[],[] -> []
+ | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
+ | _ -> assert false
+ in
+ let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
+ fl_ty' fl_bo' fl
+ in
+ C.Fix (i,fl''),ty,subst,metasenv,ugraph2
| C.CoFix (i,fl) ->
- let subst,metasenv,types,ugraph1 =
+ let fl_ty',subst,metasenv,types,ugraph1 =
List.fold_left
- (fun (subst,metasenv,types,ugraph) (n,ty,_) ->
- let _,subst',metasenv',ugraph1 = type_of_aux subst metasenv context ty ugraph in
- subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types, ugraph1
- ) (subst,metasenv,[],ugraph) fl
+ (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
+ let ty',_,subst',metasenv',ugraph1 =
+ type_of_aux subst metasenv context ty ugraph
+ in
+ fl @ [ty'],subst',metasenv',
+ Some (C.Name n,(C.Decl ty')) :: types, ugraph1
+ ) ([],subst,metasenv,[],ugraph) fl
in
let len = List.length types in
let context' = types@context in
- let subst,metasenv,ugraph2 =
+ let fl_bo',subst,metasenv,ugraph2 =
List.fold_left
- (fun (subst,metasenv,ugraph) (name,ty,bo) ->
- let ty_of_bo,subst,metasenv,ugraph1 =
+ (fun (fl,subst,metasenv,ugraph) (name,ty,bo) ->
+ let bo',ty_of_bo,subst,metasenv,ugraph1 =
type_of_aux subst metasenv context' bo ugraph
in
+ let subst',metasenv',ugraph' =
fo_unif_subst subst context' metasenv
- ty_of_bo (CicSubstitution.lift len ty) ugraph1
- ) (subst,metasenv,ugraph1) fl in
-
+ ty_of_bo (CicSubstitution.lift len ty) ugraph1
+ in
+ fl @ [bo'],subst',metasenv',ugraph'
+ ) ([],subst,metasenv,ugraph1) fl
+ in
let (_,ty,_) = List.nth fl i in
- ty,subst,metasenv,ugraph2
+ (* now we have the new ty in fl_ty', the new bo in fl_bo',
+ * and we want the new fl with bo' and ty' injected in the right
+ * place.
+ *)
+ let rec map3 f l1 l2 l3 =
+ match l1,l2,l3 with
+ | [],[],[] -> []
+ | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
+ | _ -> assert false
+ in
+ let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
+ fl_ty' fl_bo' fl
+ in
+ C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
(* check_metasenv_consistency checks that the "canonical" context of a
metavariable is consitent - up to relocation via the relocation list l -
in
try
List.fold_left2
- (fun (subst,metasenv,ugraph) t ct ->
+ (fun (l,subst,metasenv,ugraph) t ct ->
match (t,ct) with
_,None ->
- subst,metasenv,ugraph
+ l @ [None],subst,metasenv,ugraph
| Some t,Some (_,C.Def (ct,_)) ->
+ let subst',metasenv',ugraph' =
(try
fo_unif_subst subst context metasenv t ct ugraph
with e -> raise (RefineFailure (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> msg | _ -> (Printexc.to_string e)))))
+ in
+ l @ [Some t],subst',metasenv',ugraph'
| Some t,Some (_,C.Decl ct) ->
- let inferredty,subst',metasenv',ugraph1 =
+ let t',inferredty,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context t ugraph
in
+ let subst'',metasenv'',ugraph2 =
(try
fo_unif_subst
subst' context metasenv' inferredty ct ugraph1
with e -> raise (RefineFailure (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> msg | _ -> (Printexc.to_string e)))))
+ in
+ l @ [Some t'], subst'',metasenv'',ugraph2
| None, Some _ ->
raise (RefineFailure (sprintf
"Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s"
(CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
(CicMetaSubst.ppcontext subst canonical_context)))
- ) (subst,metasenv,ugraph) l lifted_canonical_context
+ ) ([],subst,metasenv,ugraph) l lifted_canonical_context
with
Invalid_argument _ ->
raise
and check_exp_named_subst metasubst metasenv context tl ugraph =
let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
match tl with
- [] -> metasubst,metasenv,ugraph
+ [] -> [],metasubst,metasenv,ugraph
| ((uri,t) as subst)::tl ->
let ty_uri,ugraph1 = type_of_variable uri ugraph in
let typeofvar =
("Unkown variable definition " ^ UriManager.string_of_uri uri))
) ;
*)
- let typeoft,metasubst',metasenv',ugraph2 =
+ let t',typeoft,metasubst',metasenv',ugraph2 =
type_of_aux metasubst metasenv context t ugraph1
in
let metasubst'',metasenv'',ugraph3 =
try
- fo_unif_subst metasubst' context metasenv' typeoft typeofvar ugraph2
+ fo_unif_subst
+ metasubst' context metasenv' typeoft typeofvar ugraph2
with _ ->
raise (RefineFailure
- ("Wrong Explicit Named Substitution: " ^ CicMetaSubst.ppterm metasubst' typeoft ^
- " not unifiable with " ^ CicMetaSubst.ppterm metasubst' typeofvar))
+ ("Wrong Explicit Named Substitution: " ^
+ CicMetaSubst.ppterm metasubst' typeoft ^
+ " not unifiable with " ^
+ CicMetaSubst.ppterm metasubst' typeofvar))
+ in
+ (* FIXME: no mere tail recursive! *)
+ let exp_name_subst, metasubst''', metasenv''', ugraph4 =
+ check_exp_named_subst_aux
+ metasubst'' metasenv'' (substs@[subst]) tl ugraph3
in
- check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl ugraph3
+ ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
in
check_exp_named_subst_aux metasubst metasenv [] tl ugraph
let rec mk_prod metasenv context =
function
[] ->
- let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv subst context in
+ let (metasenv, idx) =
+ CicMkImplicit.mk_implicit_type metasenv subst context
+ in
let irl =
CicMkImplicit.identity_relocation_list_for_metavariable context
in
metasenv,Cic.Meta (idx, irl)
| (_,argty)::tl ->
- let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv subst context in
+ let (metasenv, idx) =
+ CicMkImplicit.mk_implicit_type metasenv subst context
+ in
let irl =
CicMkImplicit.identity_relocation_list_for_metavariable context
in
in
let rec eat_prods metasenv subst context hetype ugraph =
function
- [] -> metasenv,subst,hetype,ugraph
+ | [] -> [],metasenv,subst,hetype,ugraph
| (hete, hety)::tl ->
(match hetype with
Cic.Prod (n,s,t) ->
- let subst,metasenv,ugraph1 =
+ let arg,subst,metasenv,ugraph1 =
try
- fo_unif_subst subst context metasenv hety s ugraph
+ let subst,metasenv,ugraph1 =
+ fo_unif_subst subst context metasenv hety s ugraph
+ in
+ hete,subst,metasenv,ugraph1
with exn ->
- prerr_endline (Printf.sprintf "hety=%s\ns=%s\nmetasenv=%s"
- (CicMetaSubst.ppterm subst hety)
- (CicMetaSubst.ppterm subst s)
- (CicMetaSubst.ppmetasenv metasenv subst));
- raise exn
-
- (*
- try
- fo_unif_subst subst context metasenv hety s
- with _ ->
- prerr_endline("senza subst fallisce");
- let hety = CicMetaSubst.apply_subst subst hety in
- let s = CicMetaSubst.apply_subst subst s in
- prerr_endline ("unifico = " ^(CicPp.ppterm hety));
- prerr_endline ("con = " ^(CicPp.ppterm s));
- fo_unif_subst subst context metasenv hety s *)
+ (* we search a coercion from hety to s *)
+ let coer = look_for_coercion
+ (CicMetaSubst.apply_subst subst hety)
+ (CicMetaSubst.apply_subst subst s)
+ in
+ match coer with
+ | None -> raise exn
+ | Some c ->
+ (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph
in
- (* DEBUG
- let t1 = CicMetaSubst.subst subst hete t in
- let t2 = CicSubstitution.subst hete t in
- prerr_endline ("con subst = " ^(CicPp.ppterm t1));
- prerr_endline ("senza subst = " ^(CicPp.ppterm t2));
- prerr_endline("++++++++++metasenv prima di eat_prods:\n" ^
- (CicMetaSubst.ppmetasenv metasenv subst));
- prerr_endline("++++++++++subst prima di eat_prods:\n" ^
- (CicMetaSubst.ppsubst subst));
- *)
+ let coerced_args,metasenv',subst',t',ugraph2 =
eat_prods metasenv subst context
(* (CicMetaSubst.subst subst hete t) tl *)
(CicSubstitution.subst hete t) ugraph1 tl
+ in
+ arg::coerced_args,metasenv',subst',t',ugraph2
| _ -> assert false
)
in
- let metasenv,subst,t,ugraph2 =
+ let coerced_args,metasenv,subst,t,ugraph2 =
eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
in
- t,subst,metasenv,ugraph2
- (* eat prods ends here! *)
+ coerced_args,t,subst,metasenv,ugraph2
in
- let ty,subst',metasenv',ugraph1 =
+
+ (* eat prods ends here! *)
+
+ let t',ty,subst',metasenv',ugraph1 =
type_of_aux [] metasenv context t ugraph
in
- let substituted_t = CicMetaSubst.apply_subst subst' t in
+ let substituted_t = CicMetaSubst.apply_subst subst' t' in
let substituted_ty = CicMetaSubst.apply_subst subst' ty in
(* Andrea: ho rimesso qui l'applicazione della subst al
metasenv dopo che ho droppato l'invariante che il metsaenv
projects / helm.git / commitdiff