open Printf
-exception RefineFailure of string;;
-exception Uncertain of string;;
-exception AssertFailure of string;;
+exception RefineFailure of string Lazy.t;;
+exception Uncertain of string Lazy.t;;
+exception AssertFailure of string Lazy.t;;
let debug_print = fun _ -> ()
+let profiler = HExtlib.profile "CicRefine.fo_unif"
+
let fo_unif_subst subst context metasenv t1 t2 ugraph =
try
+let foo () =
CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
+in profiler.HExtlib.profile foo ()
with
(CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
| (CicUnification.Uncertain msg) -> raise (Uncertain msg)
;;
+let enrich f =
+ function
+ RefineFailure msg -> raise (RefineFailure (f msg))
+ | Uncertain msg -> raise (Uncertain (f msg))
+ | _ -> assert false
+
let rec split l n =
match (l,n) with
(l,0) -> ([], l)
| (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
- | (_,_) -> raise (AssertFailure "split: list too short")
+ | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
+;;
+
+let exp_impl metasenv subst context term =
+ let rec aux metasenv context = function
+ | (Cic.Rel _) as t -> metasenv, t
+ | (Cic.Sort _) as t -> metasenv, t
+ | Cic.Const (uri, subst) ->
+ let metasenv', subst' = do_subst metasenv context subst in
+ metasenv', Cic.Const (uri, subst')
+ | Cic.Var (uri, subst) ->
+ let metasenv', subst' = do_subst metasenv context subst in
+ metasenv', Cic.Var (uri, subst')
+ | Cic.MutInd (uri, i, subst) ->
+ let metasenv', subst' = do_subst metasenv context subst in
+ metasenv', Cic.MutInd (uri, i, subst')
+ | Cic.MutConstruct (uri, i, j, subst) ->
+ let metasenv', subst' = do_subst metasenv context subst in
+ metasenv', Cic.MutConstruct (uri, i, j, subst')
+ | Cic.Meta (n,l) ->
+ let metasenv', l' = do_local_context metasenv context l in
+ metasenv', Cic.Meta (n, l')
+ | Cic.Implicit (Some `Type) ->
+ 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)
+ | Cic.Implicit (Some `Closed) ->
+ let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
+ metasenv', Cic.Meta (idx, [])
+ | Cic.Implicit None ->
+ let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
+ let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
+ metasenv', Cic.Meta (idx, irl)
+ | Cic.Implicit _ -> assert false
+ | Cic.Cast (te, ty) ->
+ let metasenv', ty' = aux metasenv context ty in
+ let metasenv'', te' = aux metasenv' context te in
+ metasenv'', Cic.Cast (te', ty')
+ | Cic.Prod (name, s, t) ->
+ let metasenv', s' = aux metasenv context s in
+ metasenv', Cic.Prod (name, s', t)
+ | Cic.Lambda (name, s, t) ->
+ let metasenv', s' = aux metasenv context s in
+ metasenv', Cic.Lambda (name, s', t)
+ | Cic.LetIn (name, s, t) ->
+ let metasenv', s' = aux metasenv context s in
+ metasenv', Cic.LetIn (name, s', t)
+ | Cic.Appl l when List.length l > 1 ->
+ let metasenv', l' =
+ List.fold_right
+ (fun term (metasenv, terms) ->
+ let new_metasenv, term = aux metasenv context term in
+ new_metasenv, term :: terms)
+ l (metasenv, [])
+ in
+ metasenv', Cic.Appl l'
+ | Cic.Appl _ -> assert false
+ | Cic.MutCase (uri, i, outtype, term, patterns) ->
+ let metasenv', l' =
+ List.fold_right
+ (fun term (metasenv, terms) ->
+ let new_metasenv, term = aux metasenv context term in
+ new_metasenv, term :: terms)
+ (outtype :: term :: patterns) (metasenv, [])
+ in
+ let outtype', term', patterns' =
+ match l' with
+ | outtype' :: term' :: patterns' -> outtype', term', patterns'
+ | _ -> assert false
+ in
+ metasenv', Cic.MutCase (uri, i, outtype', term', patterns')
+ | Cic.Fix (i, funs) ->
+ let metasenv', types =
+ List.fold_right
+ (fun (name, _, typ, _) (metasenv, types) ->
+ let new_metasenv, new_type = aux metasenv context typ in
+ (new_metasenv, (name, new_type) :: types))
+ funs (metasenv, [])
+ in
+ let rec combine = function
+ | ((name, index, _, body) :: funs_tl),
+ ((_, typ) :: typ_tl) ->
+ (name, index, typ, body) :: combine (funs_tl, typ_tl)
+ | [], [] -> []
+ | _ -> assert false
+ in
+ let funs' = combine (funs, types) in
+ metasenv', Cic.Fix (i, funs')
+ | Cic.CoFix (i, funs) ->
+ let metasenv', types =
+ List.fold_right
+ (fun (name, typ, _) (metasenv, types) ->
+ let new_metasenv, new_type = aux metasenv context typ in
+ (new_metasenv, (name, new_type) :: types))
+ funs (metasenv, [])
+ in
+ let rec combine = function
+ | ((name, _, body) :: funs_tl),
+ ((_, typ) :: typ_tl) ->
+ (name, typ, body) :: combine (funs_tl, typ_tl)
+ | [], [] -> []
+ | _ -> assert false
+ in
+ let funs' = combine (funs, types) in
+ metasenv', Cic.CoFix (i, funs')
+ and do_subst metasenv context subst =
+ List.fold_right
+ (fun (uri, term) (metasenv, substs) ->
+ let metasenv', term' = aux metasenv context term in
+ (metasenv', (uri, term') :: substs))
+ subst (metasenv, [])
+ and do_local_context metasenv context local_context =
+ List.fold_right
+ (fun term (metasenv, local_context) ->
+ let metasenv', term' =
+ match term with
+ | None -> metasenv, None
+ | Some term ->
+ let metasenv', term' = aux metasenv context term in
+ metasenv', Some term'
+ in
+ metasenv', term' :: local_context)
+ local_context (metasenv, [])
+ in
+ aux metasenv context term
;;
let rec type_of_constant uri ugraph =
- let module C = Cic in
- let module R = CicReduction in
- let module U = UriManager in
- (*
- let obj =
- try
- CicEnvironment.get_cooked_obj uri
- with Not_found -> assert false
- in
- *)
- let obj,u= CicEnvironment.get_obj ugraph uri in
- match obj with
- C.Constant (_,_,ty,_,_) -> ty,u
- | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
- | _ ->
- raise
- (RefineFailure ("Unknown constant definition " ^ U.string_of_uri uri))
+ let module C = Cic in
+ let module R = CicReduction in
+ let module U = UriManager in
+ let _ = CicTypeChecker.typecheck uri in
+ let obj,u =
+ try
+ CicEnvironment.get_cooked_obj ugraph uri
+ with Not_found -> assert false
+ in
+ match obj with
+ C.Constant (_,_,ty,_,_) -> ty,u
+ | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
+ | _ ->
+ raise
+ (RefineFailure (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
and type_of_variable uri ugraph =
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
- (*
- let obj =
- try
- CicEnvironment.get_cooked_obj uri
- with Not_found -> assert false
- in
- *)
- let obj,u = CicEnvironment.get_obj ugraph uri in
- match obj with
- C.Variable (_,_,ty,_,_) -> ty,u
- | _ ->
- raise
- (RefineFailure
- ("Unknown variable definition " ^ UriManager.string_of_uri uri))
+ let _ = CicTypeChecker.typecheck uri in
+ let obj,u =
+ try
+ CicEnvironment.get_cooked_obj ugraph uri
+ with Not_found -> assert false
+ in
+ match obj with
+ C.Variable (_,_,ty,_,_) -> ty,u
+ | _ ->
+ raise
+ (RefineFailure
+ (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
and type_of_mutual_inductive_defs uri i ugraph =
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
- (*
- let obj =
- try
- CicEnvironment.get_cooked_obj uri
- with Not_found -> assert false
- in
- *)
- let obj,u = CicEnvironment.get_obj ugraph uri in
- match obj with
- C.InductiveDefinition (dl,_,_,_) ->
- let (_,_,arity,_) = List.nth dl i in
- arity,u
- | _ ->
- raise
- (RefineFailure
- ("Unknown mutual inductive definition " ^ U.string_of_uri uri))
+ let _ = CicTypeChecker.typecheck uri in
+ let obj,u =
+ try
+ CicEnvironment.get_cooked_obj ugraph uri
+ with Not_found -> assert false
+ in
+ match obj with
+ C.InductiveDefinition (dl,_,_,_) ->
+ let (_,_,arity,_) = List.nth dl i in
+ arity,u
+ | _ ->
+ raise
+ (RefineFailure
+ (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
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
- (*
- let obj =
- try
- CicEnvironment.get_cooked_obj uri
- with Not_found -> assert false
- in
- *)
- let obj,u = CicEnvironment.get_obj ugraph uri in
+ let _ = CicTypeChecker.typecheck uri in
+ let obj,u =
+ try
+ CicEnvironment.get_cooked_obj ugraph uri
+ with Not_found -> assert false
+ in
match obj with
- C.InductiveDefinition (dl,_,_,_) ->
- let (_,_,_,cl) = List.nth dl i in
+ C.InductiveDefinition (dl,_,_,_) ->
+ let (_,_,_,cl) = List.nth dl i in
let (_,ty) = List.nth cl (j-1) in
ty,u
- | _ ->
- raise
- (RefineFailure
- ("Unkown mutual inductive definition " ^ U.string_of_uri uri))
+ | _ ->
+ raise
+ (RefineFailure
+ (lazy
+ ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
(* type_of_aux' is just another name (with a different scope) for type_of_aux *)
(* 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, ugraph
+ C.MutInd (_,_,_) ->
+ (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, ugraph
+ let (_,arguments) = split tl left_args_no in
+ (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
+ (* we expect that the actual type of the branch has the due
number of Prod *)
- (match R.whd ~subst context actualtype with
+ (match R.whd ~subst context actualtype with
C.Prod (name',so',de') ->
- 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])
+ 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)
+ (* 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 ugraph1
- | _ -> raise (AssertFailure "Wrong number of arguments"))
- | _ -> raise (AssertFailure "Prod or MutInd expected")
+ | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
+ | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
and type_of_aux' metasenv context t ugraph =
+ let metasenv, t = exp_impl metasenv [] context t in
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
+ (* this stops on binders, so we have to call it every time *)
match t with
- (* function *)
- C.Rel n ->
- (try
+ (* function *)
+ C.Rel n ->
+ (try
match List.nth context (n - 1) with
- Some (_,C.Decl ty) ->
+ Some (_,C.Decl ty) ->
t,S.lift n ty,subst,metasenv, ugraph
- | Some (_,C.Def (_,Some ty)) ->
+ | 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")
+ | Some (_,C.Def (bo,None)) ->
+ let ty,ugraph =
+ (* if it is in the context it must be already well-typed*)
+ CicTypeChecker.type_of_aux' ~subst metasenv context
+ (S.lift n bo) ugraph
+ in
+ t,ty,subst,metasenv,ugraph
+ | None -> raise (RefineFailure (lazy "Rel to hidden hypothesis"))
with
- _ -> raise (RefineFailure "Not a close term")
- )
- | C.Var (uri,exp_named_subst) ->
- let exp_named_subst',subst',metasenv',ugraph1 =
- check_exp_named_subst
+ _ -> raise (RefineFailure (lazy "Not a close term")))
+ | C.Var (uri,exp_named_subst) ->
+ 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
- in
- C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
- | C.Meta (n,l) ->
+ let ty =
+ CicSubstitution.subst_vars exp_named_subst' ty_uri
+ in
+ 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 l',subst',metasenv',ugraph1 =
- check_metasenv_consistency n subst metasenv context
- canonical_context l ugraph
+ check_metasenv_consistency n subst metasenv context
+ canonical_context l ugraph
in
- (* trust or check ??? *)
- C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
+ (* trust or check ??? *)
+ C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
subst', metasenv', ugraph1
- (* type_of_aux subst metasenv
- context (CicSubstitution.subst_meta l term) *)
+ (* type_of_aux subst metasenv
+ context (CicSubstitution.subst_meta l term) *)
with CicUtil.Subst_not_found _ ->
let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
let l',subst',metasenv', ugraph1 =
- check_metasenv_consistency n subst metasenv context
- canonical_context l ugraph
+ check_metasenv_consistency n subst metasenv context
+ canonical_context l ugraph
in
- C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
+ C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
subst', metasenv',ugraph1)
- | C.Sort (C.Type tno) ->
+ | 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 _ ->
+ 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 ty',_,subst',metasenv',ugraph1 =
+ | C.Implicit _ -> raise (AssertFailure (lazy "21"))
+ | C.Cast (te,ty) ->
+ let ty',_,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context ty ugraph
in
- let te',inferredty,subst'',metasenv'',ugraph2 =
+ 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
- in
- C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
- with
- _ -> raise (RefineFailure "Cast"))
- | C.Prod (name,s,t) ->
- let s',sort1,subst',metasenv',ugraph1 =
+ in
+ let subst''',metasenv''',ugraph3 =
+ fo_unif_subst subst'' context metasenv''
+ inferredty ty' ugraph2
+ in
+ C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
+ | C.Prod (name,s,t) ->
+ let carr t subst context = CicMetaSubst.apply_subst subst t in
+ let coerce_to_sort
+ in_source tgt_sort t type_to_coerce subst ctx metasenv uragph
+ =
+ let coercion_src = carr type_to_coerce subst ctx in
+ match coercion_src with
+ | Cic.Sort _ ->
+ t,type_to_coerce,subst,metasenv,ugraph
+(*
+ | Cic.Meta _ as meta when not in_source ->
+ let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in
+ let subst, metasenv, ugraph =
+ fo_unif_subst
+ subst ctx metasenv meta coercion_tgt ugraph
+ in
+ t, Cic.Sort tgt_sort, subst, metasenv, ugraph
+*)
+ | Cic.Meta _ as meta ->
+ t, meta, subst, metasenv, ugraph
+ | Cic.Cast _ as cast ->
+ t, cast, subst, metasenv, ugraph
+ | term ->
+ let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in
+ let search = CoercGraph.look_for_coercion in
+ let boh = search coercion_src coercion_tgt in
+ (match boh with
+ | CoercGraph.NoCoercion
+ | CoercGraph.NotHandled _ ->
+ raise
+ (RefineFailure (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort")))
+ | CoercGraph.NotMetaClosed ->
+ raise
+ (Uncertain (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort")))
+ | CoercGraph.SomeCoercion c ->
+ Cic.Appl [c;t],Cic.Sort tgt_sort,subst, metasenv, ugraph)
+ in
+ let s',sort1,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context s ugraph
in
- let t',sort2,subst'',metasenv'',ugraph2 =
+ let s',sort1,subst', metasenv',ugraph1 =
+ coerce_to_sort true (Cic.Type(CicUniv.fresh()))
+ s' sort1 subst' context metasenv' ugraph1
+ in
+ let context_for_t = ((Some (name,(C.Decl s')))::context) in
+ let metasenv',t = exp_impl metasenv' subst' context_for_t t in
+ let t',sort2,subst'',metasenv'',ugraph2 =
type_of_aux subst' metasenv'
- ((Some (name,(C.Decl s')))::context) t ugraph1
- in
- let sop,subst''',metasenv''',ugraph3 =
- sort_of_prod subst'' metasenv''
- context (name,s') (sort1,sort2) ugraph2
+ context_for_t t ugraph1
in
- C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
- | C.Lambda (n,s,t) ->
- let s',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 _ -> ()
- | _ ->
- raise (RefineFailure (sprintf
- "Not well-typed lambda-abstraction: the source %s should be a type;
- instead it is a term of type %s" (CicPp.ppterm s)
- (CicPp.ppterm sort1)))
- ) ;
- let t',type2,subst'',metasenv'',ugraph2 =
- type_of_aux subst' metasenv'
- ((Some (n,(C.Decl s')))::context) t ugraph1
- in
- 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 s',ty,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context s ugraph
- in
- 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.
+ let t',sort2,subst'',metasenv'',ugraph2 =
+ coerce_to_sort false (Cic.Type(CicUniv.fresh()))
+ t' sort2 subst'' context_for_t metasenv'' ugraph2
+ in
+ 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 s',sort1,subst',metasenv',ugraph1 =
+ type_of_aux subst metasenv context s ugraph in
+ let s',sort1 =
+ match CicReduction.whd ~subst:subst' context sort1 with
+ C.Meta _
+ | C.Sort _ -> s',sort1
+ | coercion_src ->
+ let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh ())) in
+ let search = CoercGraph.look_for_coercion in
+ let boh = search coercion_src coercion_tgt in
+ match boh with
+ | CoercGraph.SomeCoercion c ->
+ Cic.Appl [c;s'], coercion_tgt
+ | CoercGraph.NoCoercion
+ | CoercGraph.NotHandled _
+ | CoercGraph.NotMetaClosed ->
+ raise (RefineFailure (lazy (sprintf
+ "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s) (CicPp.ppterm sort1))))
+ in
+ let context_for_t = ((Some (n,(C.Decl s')))::context) in
+ let metasenv',t = exp_impl metasenv' subst' context_for_t t in
+ let t',type2,subst'',metasenv'',ugraph2 =
+ type_of_aux subst' metasenv' context_for_t t ugraph1
+ in
+ 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 s',ty,subst',metasenv',ugraph1 =
+ type_of_aux subst metasenv context s ugraph
+ in
+ let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
+ let metasenv',t = exp_impl metasenv' subst' context_for_t t in
+
+ let t',inferredty,subst'',metasenv'',ugraph2 =
+ type_of_aux subst' metasenv'
+ context_for_t t ugraph1
+ in
+ (* One-step LetIn reduction.
* Even faster than the previous solution.
- * Moreover the inferred type is closer to the expected one.
+ * Moreover the inferred type is closer to the expected one.
*)
- C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
+ C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
subst'',metasenv'',ugraph2
- | C.Appl (he::((_::_) as tl)) ->
- 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 x',ty,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context x ugraph
- in
- (x', ty)::res,subst',metasenv',ugraph1
- ) tl ([],subst',metasenv',ugraph1)
- in
+ | C.Appl (he::((_::_) as tl)) ->
+ 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 x',ty,subst',metasenv',ugraph1 =
+ type_of_aux subst metasenv context x ugraph
+ in
+ (x', ty)::res,subst',metasenv',ugraph1
+ ) tl ([],subst',metasenv',ugraph1)
+ in
let tl',applty,subst''',metasenv''',ugraph3 =
- eat_prods subst'' metasenv'' context
+ try
+ eat_prods true subst'' metasenv'' context
hetype tlbody_and_type ugraph2
+ with
+ exn ->
+ enrich
+ (fun msg ->
+ lazy ("The application " ^
+ CicMetaSubst.ppterm_in_context subst'' t context ^
+ " is not well typed:\n" ^ Lazy.force msg)) exn
in
C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
- | C.Appl _ -> raise (RefineFailure "Appl: no arguments")
- | C.Const (uri,exp_named_subst) ->
- let exp_named_subst',subst',metasenv',ugraph1 =
- check_exp_named_subst subst metasenv context
+ | C.Appl _ -> raise (RefineFailure (lazy "Appl: no arguments"))
+ | C.Const (uri,exp_named_subst) ->
+ 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
- in
- C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
- | C.MutInd (uri,i,exp_named_subst) ->
- let exp_named_subst',subst',metasenv',ugraph1 =
- check_exp_named_subst subst metasenv context
+ let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
+ let cty =
+ CicSubstitution.subst_vars exp_named_subst' ty_uri
+ in
+ C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
+ | C.MutInd (uri,i,exp_named_subst) ->
+ 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
- C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
- | C.MutConstruct (uri,i,j,exp_named_subst) ->
- let exp_named_subst',subst',metasenv',ugraph1 =
- check_exp_named_subst subst metasenv context
+ 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
+ C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
+ | C.MutConstruct (uri,i,j,exp_named_subst) ->
+ let exp_named_subst',subst',metasenv',ugraph1 =
+ check_exp_named_subst subst metasenv context
exp_named_subst ugraph
in
- let ty_uri,ugraph2 =
+ let ty_uri,ugraph2 =
type_of_mutual_inductive_constr uri i j ugraph1
in
- let cty =
- CicSubstitution.subst_vars exp_named_subst' ty_uri
+ let cty =
+ CicSubstitution.subst_vars exp_named_subst' ty_uri
in
- C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
+ 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)
+ | 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,ugraph =
- let obj,u = CicEnvironment.get_obj ugraph uri in
+ let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
+ let _ = CicTypeChecker.typecheck uri in
+ let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
match obj with
- C.InductiveDefinition (l,expl_params,parsno,_) ->
- List.nth l i , expl_params, parsno, u
- | _ ->
- raise
- (RefineFailure
- ("Unkown mutual inductive definition " ^
- U.string_of_uri uri))
+ C.InductiveDefinition (l,expl_params,parsno,_) ->
+ List.nth l i , expl_params, parsno, u
+ | _ ->
+ raise
+ (RefineFailure
+ (lazy ("Unkown mutual inductive definition " ^
+ U.string_of_uri uri)))
in
- let rec count_prod t =
+ let rec count_prod t =
match CicReduction.whd ~subst context t with
- C.Prod (_, _, t) -> 1 + (count_prod t)
- | _ -> 0
+ C.Prod (_, _, t) -> 1 + (count_prod t)
+ | _ -> 0
in
- let no_args = count_prod arity in
- (* now, create a "generic" MutInd *)
- let metasenv,left_args =
+ 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
- let metasenv,right_args =
+ 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
+ if no_right_params < 0 then assert false
+ else CicMkImplicit.n_fresh_metas
metasenv subst context no_right_params
in
- let metasenv,exp_named_subst =
+ let metasenv,exp_named_subst =
CicMkImplicit.fresh_subst metasenv subst context expl_params in
- let expected_type =
+ let expected_type =
if no_args = 0 then
- C.MutInd (uri,i,exp_named_subst)
+ C.MutInd (uri,i,exp_named_subst)
else
- C.Appl
+ C.Appl
(C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
- in
- (* check consistency with the actual type of term *)
- let term',actual_type,subst,metasenv,ugraph1 =
+ in
+ (* check consistency with the actual type of term *)
+ let term',actual_type,subst,metasenv,ugraph1 =
type_of_aux subst metasenv context term ugraph in
- let expected_type',_, 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 =
+ 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
- in
+ in
let rec instantiate_prod t =
function
[] -> t
in
let arity_instantiated_with_left_args =
instantiate_prod arity left_args in
- (* TODO: check if the sort elimination
+ (* TODO: check if the sort elimination
* is allowed: [(I q1 ... qr)|B] *)
- let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
+ let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
List.fold_left
- (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
+ (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 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
+ 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
+ let outtypeinstance,subst,metasenv,ugraph3 =
+ check_branch 0 context metasenv subst no_left_params
actual_type constructor' expected_type ugraph2
in
- (pl @ [p'],j+1,
+ (pl @ [p'],j+1,
outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
- ([],1,[],subst,metasenv,ugraph3) pl
+ ([],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
+ The easy case is when the outype is specified, that amount
+ to a trivial check. Otherwise, we should guess a type from
+ its instances
*)
(match outtype with
(let candidate,ugraph5,metasenv,subst =
let exp_name_subst, metasenv =
let o,_ =
- CicEnvironment.get_obj CicUniv.empty_ugraph uri
+ CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
in
let uris = CicUtil.params_of_obj o in
List.fold_right (
let metasenv,new_meta =
CicMkImplicit.mk_implicit metasenv subst extended_context
in
- let irl =
+ let irl =
CicMkImplicit.identity_relocation_list_for_metavariable
extended_context
in
None,ugraph4,metasenv,subst
in
match candidate with
- | None -> raise (Uncertain "can't solve an higher order unification problem")
+ | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
| Some candidate ->
let subst,metasenv,ugraph =
fo_unif_subst subst context metasenv
(Cic.Appl (outtype::right_args@[term']))),
subst,metasenv,ugraph)
| _ -> (* easy case *)
+ let outtype,outtypety, subst, metasenv,ugraph4 =
+ type_of_aux subst metasenv context outtype ugraph4
+ in
+ let tlbody_and_type,subst,metasenv,ugraph4 =
+ List.fold_right
+ (fun x (res,subst,metasenv,ugraph) ->
+ let x',ty,subst',metasenv',ugraph1 =
+ type_of_aux subst metasenv context x ugraph
+ in
+ (x', ty)::res,subst',metasenv',ugraph1
+ ) (right_args @ [term']) ([],subst,metasenv,ugraph4)
+ in
+ let _,_,subst,metasenv,ugraph4 =
+ eat_prods false subst metasenv context
+ outtypety tlbody_and_type ugraph4
+ in
let _,_, subst, metasenv,ugraph5 =
type_of_aux subst metasenv context
(C.Appl ((outtype :: right_args) @ [term'])) ugraph4
(CicMetaSubst.apply_subst subst
(C.Appl(outtype::right_args@[term]))),
subst,metasenv,ugraph6)
- | C.Fix (i,fl) ->
- let fl_ty',subst,metasenv,types,ugraph1 =
- List.fold_left
- (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
- let ty',_,subst',metasenv',ugraph1 =
+ | C.Fix (i,fl) ->
+ let fl_ty',subst,metasenv,types,ugraph1 =
+ List.fold_left
+ (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',
+ 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 fl_bo',subst,metasenv,ugraph2 =
+ ) ([],subst,metasenv,[],ugraph) fl
+ in
+ let len = List.length types in
+ let context' = types@context in
+ let fl_bo',subst,metasenv,ugraph2 =
List.fold_left
- (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
+ (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
+ let metasenv, bo = exp_impl metasenv subst context' bo in
+ 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
+ fo_unif_subst subst context' metasenv
+ ty_of_bo (CicSubstitution.lift len ty) ugraph1
in
fl @ [bo'] , subst',metasenv',ugraph'
- ) ([],subst,metasenv,ugraph1) fl
+ ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
in
- let (_,_,ty,_) = List.nth fl i in
+ let ty = List.nth fl_ty' i in
(* 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.
fl_ty' fl_bo' fl
in
C.Fix (i,fl''),ty,subst,metasenv,ugraph2
- | C.CoFix (i,fl) ->
- let fl_ty',subst,metasenv,types,ugraph1 =
- List.fold_left
- (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
- let ty',_,subst',metasenv',ugraph1 =
+ | C.CoFix (i,fl) ->
+ let fl_ty',subst,metasenv,types,ugraph1 =
+ List.fold_left
+ (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',
+ 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 fl_bo',subst,metasenv,ugraph2 =
+ ) ([],subst,metasenv,[],ugraph) fl
+ in
+ let len = List.length types in
+ let context' = types@context in
+ let fl_bo',subst,metasenv,ugraph2 =
List.fold_left
- (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
+ (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
+ let metasenv, bo = exp_impl metasenv subst context' bo in
+ 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
+ fo_unif_subst subst context' metasenv
ty_of_bo (CicSubstitution.lift len ty) ugraph1
in
fl @ [bo'],subst',metasenv',ugraph'
- ) ([],subst,metasenv,ugraph1) fl
+ ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
in
- let (_,ty,_) = List.nth fl i in
+ let ty = List.nth fl_ty' i in
(* 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 module S = CicSubstitution in
let lifted_canonical_context =
let rec aux i =
- function
+ function
[] -> []
- | (Some (n,C.Decl t))::tl ->
+ | (Some (n,C.Decl t))::tl ->
(Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
- | (Some (n,C.Def (t,None)))::tl ->
+ | (Some (n,C.Def (t,None)))::tl ->
(Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
- | None::tl -> None::(aux (i+1) tl)
- | (Some (n,C.Def (t,Some ty)))::tl ->
+ | None::tl -> None::(aux (i+1) tl)
+ | (Some (n,C.Def (t,Some ty)))::tl ->
(Some (n,
- C.Def ((S.subst_meta l (S.lift i t)),
- Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
+ C.Def ((S.subst_meta l (S.lift i t)),
+ Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
in
- aux 1 canonical_context
+ aux 1 canonical_context
in
try
- List.fold_left2
- (fun (l,subst,metasenv,ugraph) t ct ->
+ List.fold_left2
+ (fun (l,subst,metasenv,ugraph) t ct ->
match (t,ct) with
- _,None ->
- l @ [None],subst,metasenv,ugraph
+ _,None ->
+ 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)))))
+ (try
+ fo_unif_subst subst context metasenv t ct ugraph
+ with e -> raise (RefineFailure (lazy (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 -> Lazy.force msg | _ -> (Printexc.to_string e))))))
in
l @ [Some t],subst',metasenv',ugraph'
| Some t,Some (_,C.Decl ct) ->
- let t',inferredty,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context t ugraph
- in
+ 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)))))
+ (try
+ fo_unif_subst
+ subst' context metasenv' inferredty ct ugraph1
+ with e -> raise (RefineFailure (lazy (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 -> Lazy.force msg | RefineFailure msg -> Lazy.force 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
+ raise (RefineFailure (lazy (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
with
- Invalid_argument _ ->
- raise
- (RefineFailure
- (sprintf
- "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
- (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
- (CicMetaSubst.ppcontext subst canonical_context)))
+ Invalid_argument _ ->
+ raise
+ (RefineFailure
+ (lazy (sprintf
+ "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
+ (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
+ (CicMetaSubst.ppcontext subst canonical_context))))
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 =
+ [] -> [],metasubst,metasenv,ugraph
+ | ((uri,t) as subst)::tl ->
+ let ty_uri,ugraph1 = type_of_variable uri ugraph in
+ let typeofvar =
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,_,_) ->
- raise
- (RefineFailure
- "A variable with a body can not be explicit substituted")
- | Cic.Variable (_,None,_,_) -> ()
- | _ ->
- raise
- (RefineFailure
- ("Unkown variable definition " ^ UriManager.string_of_uri uri))
- ) ;
- *)
- let t',typeoft,metasubst',metasenv',ugraph2 =
+ (* CSC: why was this code here? it is wrong
+ (match CicEnvironment.get_cooked_obj ~trust:false uri with
+ Cic.Variable (_,Some bo,_,_) ->
+ raise
+ (RefineFailure (lazy
+ "A variable with a body can not be explicit substituted"))
+ | Cic.Variable (_,None,_,_) -> ()
+ | _ ->
+ raise
+ (RefineFailure (lazy
+ ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
+ ) ;
+ *)
+ let t',typeoft,metasubst',metasenv',ugraph2 =
type_of_aux metasubst metasenv context t ugraph1
- in
+ in
let metasubst'',metasenv'',ugraph3 =
try
- fo_unif_subst
+ fo_unif_subst
metasubst' context metasenv' typeoft typeofvar ugraph2
with _ ->
- raise (RefineFailure
- ("Wrong Explicit Named Substitution: " ^
+ raise (RefineFailure (lazy
+ ("Wrong Explicit Named Substitution: " ^
CicMetaSubst.ppterm metasubst' typeoft ^
- " not unifiable with " ^
- CicMetaSubst.ppterm metasubst' typeofvar))
+ " not unifiable with " ^
+ CicMetaSubst.ppterm metasubst' typeofvar)))
in
(* FIXME: no mere tail recursive! *)
let exp_name_subst, metasubst''', metasenv''', ugraph4 =
let t1'' = CicReduction.whd ~subst context t1 in
let t2'' = CicReduction.whd ~subst context_for_t2 t2 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 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,ugraph
- | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
- (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
- let t' = CicUniv.fresh() in
- 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,ugraph
- | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
- | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
+ | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
+ let t' = CicUniv.fresh() in
+ 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)) ->
+ 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 *)
- (* TODO if we check the non meta term and if it is a sort then we are
- * likely to know the exact value of the result e.g. if the rhs is a
- * Sort (Prop | Set | CProp) then the result is the rhs *)
+ (* TODO if we check the non meta term and if it is a sort then we
+ * are likely to know the exact value of the result e.g. if the rhs
+ * is a Sort (Prop | Set | CProp) then the result is the rhs *)
let (metasenv,idx) =
CicMkImplicit.mk_implicit_sort metasenv subst in
let (subst, metasenv,ugraph1) =
- fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' ugraph
+ fo_unif_subst subst context_for_t2 metasenv
+ (C.Meta (idx,[])) t2'' ugraph
in
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'')))
+ | _,_ ->
+ raise
+ (RefineFailure
+ (lazy
+ (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 ugraph =
+ and eat_prods
+ allow_coercions subst metasenv context hetype tlbody_and_type ugraph
+ =
let rec mk_prod metasenv context =
function
- [] ->
- let (metasenv, idx) =
+ [] ->
+ let (metasenv, idx) =
CicMkImplicit.mk_implicit_type metasenv subst context
in
- let irl =
+ let irl =
CicMkImplicit.identity_relocation_list_for_metavariable context
- in
+ in
metasenv,Cic.Meta (idx, irl)
- | (_,argty)::tl ->
- let (metasenv, idx) =
+ | (_,argty)::tl ->
+ let (metasenv, idx) =
CicMkImplicit.mk_implicit_type metasenv subst context
in
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context
- in
- let meta = Cic.Meta (idx,irl) in
- let name =
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context
+ in
+ let meta = Cic.Meta (idx,irl) in
+ let name =
(* The name must be fresh for context. *)
(* Nevertheless, argty is well-typed only in context. *)
(* Thus I generate a name (name_hint) in context and *)
(* then I generate a name --- using the hint name_hint *)
(* --- that is fresh in (context'@context). *)
let name_hint =
- (* Cic.Name "pippo" *)
- FreshNamesGenerator.mk_fresh_name ~subst metasenv
- (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
- (CicMetaSubst.apply_subst_context subst context)
- Cic.Anonymous
- ~typ:(CicMetaSubst.apply_subst subst argty)
+ (* Cic.Name "pippo" *)
+ FreshNamesGenerator.mk_fresh_name ~subst metasenv
+ (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
+ (CicMetaSubst.apply_subst_context subst context)
+ Cic.Anonymous
+ ~typ:(CicMetaSubst.apply_subst subst argty)
in
- (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
- FreshNamesGenerator.mk_fresh_name ~subst
- [] context name_hint ~typ:(Cic.Sort Cic.Prop)
- in
- let metasenv,target =
+ (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
+ FreshNamesGenerator.mk_fresh_name ~subst
+ [] context name_hint ~typ:(Cic.Sort Cic.Prop)
+ in
+ let metasenv,target =
mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
- in
+ in
metasenv,Cic.Prod (name,meta,target)
in
let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
let (subst, metasenv,ugraph1) =
try
- fo_unif_subst subst context metasenv hetype hetype' ugraph
+ fo_unif_subst subst context metasenv hetype hetype' ugraph
with exn ->
- debug_print (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
- (CicPp.ppterm hetype)
- (CicPp.ppterm hetype')
- (CicMetaSubst.ppmetasenv metasenv [])
- (CicMetaSubst.ppsubst subst));
- raise exn
+ debug_print (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
+ (CicPp.ppterm hetype)
+ (CicPp.ppterm hetype')
+ (CicMetaSubst.ppmetasenv [] metasenv)
+ (CicMetaSubst.ppsubst subst)));
+ raise exn
in
let rec eat_prods metasenv subst context hetype ugraph =
function
| [] -> [],metasenv,subst,hetype,ugraph
- | (hete, hety)::tl ->
+ | (hete, hety)::tl ->
(match hetype with
- Cic.Prod (n,s,t) ->
- let arg,subst,metasenv,ugraph1 =
- try
+ Cic.Prod (n,s,t) ->
+ let arg,subst,metasenv,ugraph1 =
+ try
let subst,metasenv,ugraph1 =
fo_unif_subst subst context metasenv hety s ugraph
in
hete,subst,metasenv,ugraph1
- with exn ->
+ with exn when allow_coercions ->
(* we search a coercion from hety to s *)
- let coer = CoercGraph.look_for_coercion
- (CicMetaSubst.apply_subst subst hety)
- (CicMetaSubst.apply_subst subst s)
+ let coer =
+ let carr t subst context =
+ CicMetaSubst.apply_subst subst t
+ in
+ let c_hety = carr hety subst context in
+ let c_s = carr s subst context in
+ CoercGraph.look_for_coercion c_hety c_s
in
match coer with
- | None -> raise exn
- | Some c ->
+ | CoercGraph.NoCoercion
+ | CoercGraph.NotHandled _ ->
+ let msg e =
+ lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst hete
+ context ^ " has type " ^
+ CicMetaSubst.ppterm_in_context subst hety
+ context ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context subst s context
+ (* "\nReason: " ^ Lazy.force e*))
+ in
+ enrich msg exn
+ | CoercGraph.NotMetaClosed ->
+ raise (Uncertain (lazy "Coercions on meta"))
+ | CoercGraph.SomeCoercion c ->
(Cic.Appl [ c ; hete ]), subst, metasenv, ugraph
- in
+ in
let coerced_args,metasenv',subst',t',ugraph2 =
- eat_prods metasenv subst context
- (* (CicMetaSubst.subst subst hete t) tl *)
- (CicSubstitution.subst hete t) ugraph1 tl
+ eat_prods metasenv subst context
+ (CicSubstitution.subst arg t) ugraph1 tl
in
arg::coerced_args,metasenv',subst',t',ugraph2
| _ -> assert false
let context' =
List.map
(function
- None -> None
- | Some (n, Cic.Decl t) ->
- Some (n,
- Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
- | Some (n, Cic.Def (bo,ty)) ->
- let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
- let ty' =
+ None -> None
+ | Some (n, Cic.Decl t) ->
+ Some (n,
+ Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
+ | Some (n, Cic.Def (bo,ty)) ->
+ let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
+ let ty' =
match ty with
- None -> None
- | Some ty ->
- Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
- in
+ None -> None
+ | Some ty ->
+ Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
+ in
Some (n, Cic.Def (bo',ty'))
) context
in
try
type_of_aux' metasenv context term ugraph
with
- CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)
+ CicUniv.UniverseInconsistency msg -> raise (RefineFailure (lazy msg))
-(*CSC: this is a very very rough approximation; to be finished *)
-let are_all_occurrences_positive uri =
- let rec aux =
- (*CSC: here we should do a whd; but can we do that? *)
- function
- Cic.Appl (Cic.MutInd (uri',_,_)::_) when uri = uri' -> ()
- | Cic.MutInd (uri',_,_) when uri = uri' -> ()
- | Cic.Prod (_,_,t) -> aux t
- | _ -> raise (RefineFailure "not well formed constructor type")
- in
- aux
+let undebrujin uri typesno tys t =
+ snd
+ (List.fold_right
+ (fun (name,_,_,_) (i,t) ->
+ (* here the explicit_named_substituion is assumed to be *)
+ (* of length 0 *)
+ let t' = Cic.MutInd (uri,i,[]) in
+ let t = CicSubstitution.subst t' t in
+ i - 1,t
+ ) tys (typesno - 1,t))
+
+let map_first_n n start f g l =
+ let rec aux acc k l =
+ if k < n then
+ match l with
+ | [] -> raise (Invalid_argument "map_first_n")
+ | hd :: tl -> f hd k (aux acc (k+1) tl)
+ else
+ g acc l
+ in
+ aux start 0 l
+
+(*CSC: this is a very rough approximation; to be finished *)
+let are_all_occurrences_positive metasenv ugraph uri tys leftno =
+ let number_of_types = List.length tys in
+ let subst,metasenv,ugraph,tys =
+ List.fold_right
+ (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
+ let subst,metasenv,ugraph,cl =
+ List.fold_right
+ (fun (name,ty) (subst,metasenv,ugraph,acc) ->
+ let rec aux ctx k subst = function
+ | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
+ let subst,metasenv,ugraph,tl =
+ map_first_n leftno
+ (subst,metasenv,ugraph,[])
+ (fun t n (subst,metasenv,ugraph,acc) ->
+ let subst,metasenv,ugraph =
+ fo_unif_subst
+ subst ctx metasenv t (Cic.Rel (k-n)) ugraph
+ in
+ subst,metasenv,ugraph,(t::acc))
+ (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
+ tl
+ in
+ subst,metasenv,ugraph,(Cic.Appl (hd::tl))
+ | Cic.MutInd(uri',_,_) as t when uri = uri'->
+ subst,metasenv,ugraph,t
+ | Cic.Prod (name,s,t) ->
+ let ctx = (Some (name,Cic.Decl s))::ctx in
+ let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
+ subst,metasenv,ugraph,Cic.Prod (name,s,t)
+ | _ ->
+ raise
+ (RefineFailure
+ (lazy "not well formed constructor type"))
+ in
+ let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
+ subst,metasenv,ugraph,(name,ty) :: acc)
+ cl (subst,metasenv,ugraph,[])
+ in
+ subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
+ tys ([],metasenv,ugraph,[])
+ in
+ let substituted_tys =
+ List.map
+ (fun (name,ind,arity,cl) ->
+ let cl =
+ List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
+ in
+ name,ind,CicMetaSubst.apply_subst subst arity,cl)
+ tys
+ in
+ metasenv,ugraph,substituted_tys
let typecheck metasenv uri obj =
let ugraph = CicUniv.empty_ugraph in
(* instead of raising Uncertain, let's hope that the meta will become
a sort *)
| Cic.Meta _ -> ()
- | _ -> raise (RefineFailure "The term provided is not a type")
+ | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
end;
let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
let bo' = CicMetaSubst.apply_subst subst bo' in
let ty = CicTypeChecker.debrujin_constructor uri typesno ty in
let ty',_,metasenv,ugraph =
type_of_aux' metasenv con_context ty ugraph in
- let undebrujin t =
- snd
- (List.fold_right
- (fun (name,_,_,_) (i,t) ->
- (* here the explicit_named_substituion is assumed to be *)
- (* of length 0 *)
- let t' = Cic.MutInd (uri,i,[]) in
- let t = CicSubstitution.subst t' t in
- i - 1,t
- ) tys (typesno - 1,t)) in
- let ty' = undebrujin ty' in
+ let ty' = undebrujin uri typesno tys ty' in
metasenv,ugraph,(name,ty')::res
) cl (metasenv,ugraph,[])
in
metasenv,ugraph,(name,b,ty,cl')::res
) tys (metasenv,ugraph,[]) in
(* third phase: we check the positivity condition *)
- List.iter
- (fun (_,_,_,cl) ->
- List.iter (fun (_,ty) -> are_all_occurrences_positive uri ty) cl
- ) tys ;
+ let metasenv,ugraph,tys =
+ are_all_occurrences_positive metasenv ugraph uri tys paramsno
+ in
Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
(* DEBUGGING ONLY
try
let (t,ty,m) =
type_of_aux' metasenv context term in
- debug_print
- ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
- debug_print
- ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []);
+ debug_print (lazy
+ ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
+ debug_print (lazy
+ ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
(t,ty,m)
with
| RefineFailure msg as e ->
- debug_print ("@@@ REFINE FAILED: " ^ msg);
+ debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
raise e
| Uncertain msg as e ->
- debug_print ("@@@ REFINE UNCERTAIN: " ^ msg);
+ debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
raise e
;; *)
+
+let profiler2 = HExtlib.profile "CicRefine"
+
+let type_of_aux' metasenv context term ugraph =
+ profiler2.HExtlib.profile (type_of_aux' metasenv context term) ugraph
+
+let typecheck metasenv uri obj =
+ profiler2.HExtlib.profile (typecheck metasenv uri) obj
projects / helm.git / blobdiff