let debug_print = prerr_endline
-let fo_unif_subst subst context metasenv t1 t2 =
- try
- CicUnification.fo_unif_subst subst context metasenv t1 t2
- with
- (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
- | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
+let fo_unif_subst subst context metasenv t1 t2 ugraph =
+ try
+ CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
+ with
+ (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
+ | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
;;
let rec split l n =
| (_,_) -> raise (AssertFailure "split: list too short")
;;
-let rec type_of_constant uri =
+let rec type_of_constant uri ugraph =
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
with Not_found -> assert false
in
*)
- match CicEnvironment.get_obj uri with
- C.Constant (_,_,ty,_) -> ty
- | C.CurrentProof (_,_,_,ty,_) -> ty
+ let obj,u= CicEnvironment.get_obj uri ugraph in
+ match obj with
+ C.Constant (_,_,ty,_) -> ty,u
+ | C.CurrentProof (_,_,_,ty,_) -> ty,u
| _ ->
raise
(RefineFailure ("Unknown constant definition " ^ U.string_of_uri uri))
-and type_of_variable uri =
+and type_of_variable uri ugraph =
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
with Not_found -> assert false
in
*)
- match CicEnvironment.get_obj uri with
- C.Variable (_,_,ty,_) -> ty
+ let obj,u = CicEnvironment.get_obj uri ugraph in
+ match obj with
+ C.Variable (_,_,ty,_) -> ty,u
| _ ->
raise
(RefineFailure
("Unknown variable definition " ^ UriManager.string_of_uri uri))
-and type_of_mutual_inductive_defs uri i =
+and type_of_mutual_inductive_defs uri i ugraph =
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
with Not_found -> assert false
in
*)
- match CicEnvironment.get_obj uri with
+ let obj,u = CicEnvironment.get_obj uri ugraph in
+ match obj with
C.InductiveDefinition (dl,_,_) ->
let (_,_,arity,_) = List.nth dl i in
- arity
+ arity,u
| _ ->
raise
(RefineFailure
("Unknown mutual inductive definition " ^ U.string_of_uri uri))
-and type_of_mutual_inductive_constr uri i j =
+and type_of_mutual_inductive_constr uri i j ugraph =
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
with Not_found -> assert false
in
*)
- match CicEnvironment.get_obj uri with
+ let obj,u = CicEnvironment.get_obj uri ugraph in
+ match obj with
C.InductiveDefinition (dl,_,_) ->
let (_,_,_,cl) = List.nth dl i in
let (_,ty) = List.nth cl (j-1) in
- ty
+ ty,u
| _ ->
raise
(RefineFailure
("Unkown mutual inductive definition " ^ U.string_of_uri uri))
+
(* type_of_aux' is just another name (with a different scope) for type_of_aux *)
(* the check_branch function checks if a branch of a case is refinable.
The problem is that outype is in general unknown, and we should
try to synthesize it from the above information, that is in general
a second order unification problem. *)
-
-and check_branch n context metasenv subst left_args_no actualtype term expectedtype =
+
+and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
let module C = Cic in
(* let module R = CicMetaSubst in *)
let module R = CicReduction in
match R.whd ~subst context expectedtype with
C.MutInd (_,_,_) ->
- (n,context,actualtype, [term]), subst, metasenv
+ (n,context,actualtype, [term]), subst, metasenv, ugraph
| C.Appl (C.MutInd (_,_,_)::tl) ->
let (_,arguments) = split tl left_args_no in
- (n,context,actualtype, arguments@[term]), subst, metasenv
+ (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
| C.Prod (name,so,de) ->
(* we expect that the actual type of the branch has the due
number of Prod *)
(match R.whd ~subst context actualtype with
C.Prod (name',so',de') ->
- let subst, metasenv =
- fo_unif_subst subst context metasenv so so' in
+ let subst, metasenv, ugraph1 =
+ fo_unif_subst subst context metasenv so so' ugraph in
let term' =
(match CicSubstitution.lift 1 term with
C.Appl l -> C.Appl (l@[C.Rel 1])
| t -> C.Appl [t ; C.Rel 1]) in
(* we should also check that the name variable is anonymous in
the actual type de' ?? *)
- check_branch (n+1) ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de
+ check_branch (n+1) ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de ugraph1
| _ -> raise (AssertFailure "Wrong number of arguments"))
| _ -> raise (AssertFailure "Prod or MutInd expected")
-and type_of_aux' metasenv context t =
- let rec type_of_aux subst metasenv context t =
+and type_of_aux' metasenv context t ugraph =
+ let rec type_of_aux subst metasenv context t ugraph =
let module C = Cic in
let module S = CicSubstitution in
let module U = UriManager in
C.Rel n ->
(try
match List.nth context (n - 1) with
- Some (_,C.Decl t) -> S.lift n t,subst,metasenv
- | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv
+ 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.Def (bo,None)) ->
- type_of_aux subst metasenv context (S.lift n bo)
+ type_of_aux subst metasenv context (S.lift n bo) ugraph
| None -> raise (RefineFailure "Rel to hidden hypothesis")
with
_ -> raise (RefineFailure "Not a close term")
)
| C.Var (uri,exp_named_subst) ->
- let subst',metasenv' =
- check_exp_named_subst subst metasenv context exp_named_subst in
+ 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 ty =
- CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
+ CicSubstitution.subst_vars exp_named_subst ty_uri
in
- ty,subst',metasenv'
+ ty,subst',metasenv',ugraph1
| C.Meta (n,l) ->
(try
let (canonical_context, term,ty) = CicUtil.lookup_subst n subst in
- let subst,metasenv =
+ let subst,metasenv,ugraph1 =
check_metasenv_consistency n subst metasenv context
- canonical_context l
+ canonical_context l ugraph
in
(* trust or check ??? *)
- CicSubstitution.lift_meta l ty, subst, metasenv
+ 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 =
+ let subst,metasenv, ugraph1 =
check_metasenv_consistency n subst metasenv context
- canonical_context l
+ canonical_context l ugraph
in
- CicSubstitution.lift_meta l ty, subst, metasenv)
- (* TASSI: CONSTRAINT *)
+ CicSubstitution.lift_meta l ty, subst, metasenv,ugraph1)
+ (* TASSI: CONSTRAINT *)
| C.Sort (C.Type t) ->
let t' = CicUniv.fresh() in
- if not (CicUniv.add_gt t' t ) then
- assert false (* t' is fresh! an error in CicUniv *)
- else
- C.Sort (C.Type t'),subst,metasenv
- (* TASSI: CONSTRAINT *)
- | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())),subst,metasenv
+ 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.Implicit _ -> raise (AssertFailure "21")
| C.Cast (te,ty) ->
- let _,subst',metasenv' =
- type_of_aux subst metasenv context ty in
- let inferredty,subst'',metasenv'' =
- type_of_aux subst' metasenv' context te
+ let _,subst',metasenv',ugraph1 =
+ type_of_aux subst metasenv context ty ugraph in
+ let inferredty,subst'',metasenv'',ugraph2 =
+ type_of_aux subst' metasenv' context te ugraph1
in
(try
- let subst''',metasenv''' =
- fo_unif_subst subst'' context metasenv'' inferredty ty
+ let subst''',metasenv''',ugraph3 =
+ fo_unif_subst subst'' context metasenv'' inferredty ty ugraph2
in
- ty,subst''',metasenv'''
+ ty,subst''',metasenv''',ugraph3
with
_ -> raise (RefineFailure "Cast"))
| C.Prod (name,s,t) ->
- let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
- let sort2,subst'',metasenv'' =
- type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) 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
in
- sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
+ sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2) ugraph2
| C.Lambda (n,s,t) ->
- let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
+ let sort1,subst',metasenv',ugraph1 =
+ type_of_aux subst metasenv context s ugraph
+ in
(match CicReduction.whd ~subst:subst' context sort1 with
C.Meta _
| C.Sort _ -> ()
instead it is a term of type %s" (CicPp.ppterm s)
(CicPp.ppterm sort1)))
) ;
- let type2,subst'',metasenv'' =
- type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
+ let 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''
+ 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' = type_of_aux subst metasenv context s in
- let inferredty,subst'',metasenv'' =
- type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t
+ let 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
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'
+ CicSubstitution.subst s inferredty,subst',metasenv',ugraph2
| C.Appl (he::((_::_) as tl)) ->
- let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
- let tlbody_and_type,subst'',metasenv'' =
+ let 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) ->
- let ty,subst',metasenv' =
- type_of_aux subst metasenv context x
+ (fun x (res,subst,metasenv,ugraph) ->
+ let ty,subst',metasenv',ugraph1 =
+ type_of_aux subst metasenv context x ugraph
in
- (x, ty)::res,subst',metasenv'
- ) tl ([],subst',metasenv')
+ (x, ty)::res,subst',metasenv',ugraph1
+ ) tl ([],subst',metasenv',ugraph1)
in
- eat_prods subst'' metasenv'' context hetype tlbody_and_type
+ eat_prods subst'' metasenv'' context hetype tlbody_and_type ugraph2
| C.Appl _ -> raise (RefineFailure "Appl: no arguments")
| C.Const (uri,exp_named_subst) ->
- let subst',metasenv' =
- check_exp_named_subst subst metasenv context exp_named_subst in
+ let 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 (type_of_constant uri)
+ CicSubstitution.subst_vars exp_named_subst ty_uri
in
- cty,subst',metasenv'
+ cty,subst',metasenv',ugraph2
| C.MutInd (uri,i,exp_named_subst) ->
- let subst',metasenv' =
- check_exp_named_subst subst metasenv context exp_named_subst in
- let cty =
- CicSubstitution.subst_vars exp_named_subst
- (type_of_mutual_inductive_defs uri i)
+ let subst',metasenv',ugraph1 =
+ check_exp_named_subst subst metasenv context exp_named_subst ugraph
in
- cty,subst',metasenv'
+ 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
| C.MutConstruct (uri,i,j,exp_named_subst) ->
- let subst',metasenv' =
- check_exp_named_subst subst metasenv context exp_named_subst in
+ 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 cty =
- CicSubstitution.subst_vars exp_named_subst
- (type_of_mutual_inductive_constr uri i j)
- in
- cty,subst',metasenv'
+ CicSubstitution.subst_vars exp_named_subst ty_uri in
+ cty,subst',metasenv',ugraph2
| C.MutCase (uri, i, outtype, term, pl) ->
(* first, get the inductive type (and noparams) in the environment *)
- let (_,b,arity,constructors), expl_params, no_left_params =
+ let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
(*
let obj =
try
with Not_found -> assert false
in
*)
- match CicEnvironment.get_obj uri with
+ let obj,u = CicEnvironment.get_obj uri ugraph in
+ match obj with
C.InductiveDefinition (l,expl_params,parsno) ->
- List.nth l i , expl_params, parsno
+ List.nth l i , expl_params, parsno, u
| _ ->
raise
(RefineFailure
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 =
- type_of_aux subst metasenv context term in
- let _, subst, metasenv =
- type_of_aux subst metasenv context expected_type
+ let actual_type,subst,metasenv,ugraph1 =
+ type_of_aux subst metasenv context term ugraph in
+ let _, 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 =
- fo_unif_subst subst context metasenv expected_type actual_type
+ let subst,metasenv,ugraph3 =
+ 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) =
+ let (_,outtypeinstances,subst,metasenv,ugraph4) =
List.fold_left
- (fun (j,outtypeinstances,subst,metasenv) p ->
+ (fun (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 =
- type_of_aux subst metasenv context p in
- let expected_type, subst, metasenv =
- type_of_aux subst metasenv context constructor in
- let outtypeinstance,subst,metasenv =
+ 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 outtypeinstance,subst,metasenv,ugraph3 =
check_branch
0 context metasenv subst
- no_left_params actual_type constructor expected_type in
- (j+1,outtypeinstance::outtypeinstances,subst,metasenv))
- (1,[],subst,metasenv) pl in
+ no_left_params actual_type constructor expected_type ugraph2 in
+ (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 =
+ let _, subst, metasenv,ugraph5 =
type_of_aux subst metasenv context
- (C.Appl ((outtype :: right_args) @ [term]))
+ (C.Appl ((outtype :: right_args) @ [term])) ugraph4
in
- let (subst,metasenv) =
+ let (subst,metasenv,ugraph6) =
List.fold_left
- (fun (subst,metasenv) (constructor_args_no,context,instance,args) ->
+ (fun (subst,metasenv,ugraph) (constructor_args_no,context,instance,args) ->
let instance' =
let appl =
let outtype' =
(*
(* if appl is not well typed then the type_of below solves the
* problem *)
- let (_, subst, metasenv) =
- type_of_aux subst metasenv context appl
+ let (_, subst, metasenv,ugraph1) =
+ type_of_aux subst metasenv context appl ugraph
in
*)
(* DEBUG
(* CicMetaSubst.whd subst context appl *)
CicReduction.whd ~subst context appl
in
- fo_unif_subst subst context metasenv instance instance')
- (subst,metasenv) outtypeinstances 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
+ context (C.Appl(outtype::right_args@[term])),subst,metasenv,ugraph6
| C.Fix (i,fl) ->
- let subst,metasenv,types =
+ let subst,metasenv,types,ugraph1 =
List.fold_left
- (fun (subst,metasenv,types) (n,_,ty,_) ->
- let _,subst',metasenv' = type_of_aux subst metasenv context ty in
- subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
- ) (subst,metasenv,[]) fl
+ (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
in
let len = List.length types in
let context' = types@context in
- let subst,metasenv =
+ let subst,metasenv,ugraph2 =
List.fold_left
- (fun (subst,metasenv) (name,x,ty,bo) ->
- let ty_of_bo,subst,metasenv =
- type_of_aux subst metasenv context' bo
+ (fun (subst,metasenv,ugraph) (name,x,ty,bo) ->
+ let ty_of_bo,subst,metasenv,ugraph1 =
+ type_of_aux subst metasenv context' bo ugraph
in
fo_unif_subst subst context' metasenv
- ty_of_bo (CicSubstitution.lift len ty)
- ) (subst,metasenv) fl in
+ ty_of_bo (CicSubstitution.lift len ty) ugraph1
+ ) (subst,metasenv,ugraph1) fl in
let (_,_,ty,_) = List.nth fl i in
- ty,subst,metasenv
+ ty,subst,metasenv,ugraph2
| C.CoFix (i,fl) ->
- let subst,metasenv,types =
+ let subst,metasenv,types,ugraph1 =
List.fold_left
- (fun (subst,metasenv,types) (n,ty,_) ->
- let _,subst',metasenv' = type_of_aux subst metasenv context ty in
- subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
- ) (subst,metasenv,[]) fl
+ (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
in
let len = List.length types in
let context' = types@context in
- let subst,metasenv =
+ let subst,metasenv,ugraph2 =
List.fold_left
- (fun (subst,metasenv) (name,ty,bo) ->
- let ty_of_bo,subst,metasenv =
- type_of_aux subst metasenv context' bo
+ (fun (subst,metasenv,ugraph) (name,ty,bo) ->
+ let ty_of_bo,subst,metasenv,ugraph1 =
+ type_of_aux subst metasenv context' bo ugraph
in
fo_unif_subst subst context' metasenv
- ty_of_bo (CicSubstitution.lift len ty)
- ) (subst,metasenv) fl in
+ ty_of_bo (CicSubstitution.lift len ty) ugraph1
+ ) (subst,metasenv,ugraph1) fl in
let (_,ty,_) = List.nth fl i in
- ty,subst,metasenv
+ 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 -
with the actual context *)
and check_metasenv_consistency
- metano subst metasenv context canonical_context l
+ metano subst metasenv context canonical_context l ugraph
=
let module C = Cic in
let module R = CicReduction in
in
try
List.fold_left2
- (fun (subst,metasenv) t ct ->
+ (fun (subst,metasenv,ugraph) t ct ->
match (t,ct) with
_,None ->
- subst,metasenv
+ subst,metasenv,ugraph
| Some t,Some (_,C.Def (ct,_)) ->
(try
- fo_unif_subst subst context metasenv t ct
+ 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)))))
| Some t,Some (_,C.Decl ct) ->
- let inferredty,subst',metasenv' =
- type_of_aux subst metasenv context t
+ let inferredty,subst',metasenv',ugraph1 =
+ type_of_aux subst metasenv context t ugraph
in
(try
fo_unif_subst
- subst' context metasenv' inferredty ct
+ 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)))))
| 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) l lifted_canonical_context
+ ) (subst,metasenv,ugraph) l lifted_canonical_context
with
Invalid_argument _ ->
raise
(CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
(CicMetaSubst.ppcontext subst canonical_context)))
- and check_exp_named_subst metasubst metasenv context =
- let rec check_exp_named_subst_aux metasubst metasenv substs =
- function
- [] -> metasubst,metasenv
+ 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
| ((uri,t) as subst)::tl ->
+ let ty_uri,ugraph1 = type_of_variable uri ugraph in
let typeofvar =
- CicSubstitution.subst_vars substs (type_of_variable uri) in
+ CicSubstitution.subst_vars substs ty_uri in
(* CSC: why was this code here? it is wrong
(match CicEnvironment.get_cooked_obj ~trust:false uri with
Cic.Variable (_,Some bo,_,_) ->
("Unkown variable definition " ^ UriManager.string_of_uri uri))
) ;
*)
- let typeoft,metasubst',metasenv' =
- type_of_aux metasubst metasenv context t
+ let typeoft,metasubst',metasenv',ugraph2 =
+ type_of_aux metasubst metasenv context t ugraph1
in
- let metasubst'',metasenv'' =
+ let metasubst'',metasenv'',ugraph3 =
try
- fo_unif_subst metasubst' context metasenv' typeoft typeofvar
+ 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))
in
- check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
+ check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl ugraph3
in
- check_exp_named_subst_aux metasubst metasenv []
+ check_exp_named_subst_aux metasubst metasenv [] tl ugraph
- and sort_of_prod subst metasenv context (name,s) (t1, t2) =
+
+ and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
let module C = Cic in
let context_for_t2 = (Some (name,C.Decl s))::context in
let t1'' = CicReduction.whd ~subst context t1 in
match (t1'', t2'') with
(C.Sort s1, C.Sort s2)
when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
- C.Sort s2,subst,metasenv
+ C.Sort s2,subst,metasenv,ugraph
| (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
(* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
let t' = CicUniv.fresh() in
- if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then
- assert false ; (* not possible, error in CicUniv *)
- C.Sort (C.Type t'),subst,metasenv
+ let ugraph1 = CicUniv.add_ge t' t1 ugraph in
+ let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+ C.Sort (C.Type t'),subst,metasenv,ugraph2
| (C.Sort _,C.Sort (C.Type t1)) ->
(* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
- C.Sort (C.Type t1),subst,metasenv
- | (C.Meta _, C.Sort _) -> t2'',subst,metasenv
+ C.Sort (C.Type t1),subst,metasenv,ugraph
+ | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
| (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
(* TODO how can we force the meta to become a sort? If we don't we
* brake the invariant that refine produce only well typed terms *)
* Sort (Prop | Set | CProp) then the result is the rhs *)
let (metasenv,idx) =
CicMkImplicit.mk_implicit_sort metasenv subst in
- let (subst, metasenv) =
- fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2''
+ let (subst, metasenv,ugraph1) =
+ fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' ugraph
in
- t2'',subst,metasenv
+ t2'',subst,metasenv,ugraph1
| (_,_) ->
raise (RefineFailure (sprintf
"Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
(CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
(CicPp.ppterm t2'')))
- and eat_prods subst metasenv context hetype tlbody_and_type =
+ and eat_prods subst metasenv context hetype tlbody_and_type ugraph =
let rec mk_prod metasenv context =
function
[] ->
metasenv,Cic.Prod (name,meta,target)
in
let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
- let (subst, metasenv) =
+ let (subst, metasenv,ugraph1) =
try
- fo_unif_subst subst context metasenv hetype hetype'
+ fo_unif_subst subst context metasenv hetype hetype' ugraph
with exn ->
prerr_endline (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
(CicPp.ppterm hetype)
raise exn
in
- let rec eat_prods metasenv subst context hetype =
+ let rec eat_prods metasenv subst context hetype ugraph =
function
- [] -> metasenv,subst,hetype
+ [] -> metasenv,subst,hetype,ugraph
| (hete, hety)::tl ->
(match hetype with
Cic.Prod (n,s,t) ->
- let subst,metasenv =
+ let subst,metasenv,ugraph1 =
try
- fo_unif_subst subst context metasenv hety s
+ fo_unif_subst subst context metasenv hety s ugraph
with exn ->
prerr_endline (Printf.sprintf "hety=%s\ns=%s\nmetasenv=%s"
(CicMetaSubst.ppterm subst hety)
*)
eat_prods metasenv subst context
(* (CicMetaSubst.subst subst hete t) tl *)
- (CicSubstitution.subst hete t) tl
+ (CicSubstitution.subst hete t) ugraph1 tl
| _ -> assert false
)
in
- let metasenv,subst,t =
- eat_prods metasenv subst context hetype' tlbody_and_type
+ let metasenv,subst,t,ugraph2 =
+ eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
in
- t,subst,metasenv
+ t,subst,metasenv,ugraph2
(* eat prods ends here! *)
in
- let ty,subst',metasenv' =
- type_of_aux [] metasenv context t
+ let ty,subst',metasenv',ugraph1 =
+ type_of_aux [] metasenv context t ugraph
in
let substituted_t = CicMetaSubst.apply_subst subst' t in
let substituted_ty = CicMetaSubst.apply_subst subst' ty in
(n,context',ty')
) substituted_metasenv
in
- (cleaned_t,cleaned_ty,cleaned_metasenv)
+ (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
;;
-
-
(* DEBUGGING ONLY
let type_of_aux' metasenv context term =
try
projects / helm.git / blobdiff