;;
let rec type_of_constant uri =
- 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
- match obj with
- C.Constant (_,_,ty,_) -> ty
- | C.CurrentProof (_,_,_,ty,_) -> ty
- | _ ->
- 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 obj =
+ try
+ CicEnvironment.get_cooked_obj uri
+ with Not_found -> assert false
+ in
+ *)
+ match CicEnvironment.get_obj uri with
+ C.Constant (_,_,ty,_) -> ty
+ | C.CurrentProof (_,_,_,ty,_) -> ty
+ | _ ->
+ raise
+ (RefineFailure ("Unknown constant definition " ^ U.string_of_uri uri))
and type_of_variable uri =
- 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
- match obj with
- C.Variable (_,_,ty,_) -> ty
- | _ ->
- raise
- (RefineFailure
- ("Unknown variable definition " ^ UriManager.string_of_uri uri))
+ 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
+ *)
+ match CicEnvironment.get_obj uri with
+ C.Variable (_,_,ty,_) -> ty
+ | _ ->
+ raise
+ (RefineFailure
+ ("Unknown variable definition " ^ UriManager.string_of_uri uri))
and type_of_mutual_inductive_defs uri i =
- 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
- match obj with
- C.InductiveDefinition (dl,_,_) ->
- let (_,_,arity,_) = List.nth dl i in
- arity
- | _ ->
- raise
- (RefineFailure
- ("Unknown mutual inductive definition " ^ U.string_of_uri uri))
+ 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
+ *)
+ match CicEnvironment.get_obj uri with
+ C.InductiveDefinition (dl,_,_) ->
+ let (_,_,arity,_) = List.nth dl i in
+ arity
+ | _ ->
+ raise
+ (RefineFailure
+ ("Unknown mutual inductive definition " ^ U.string_of_uri uri))
and type_of_mutual_inductive_constr uri i j =
- 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
- match obj with
- C.InductiveDefinition (dl,_,_) ->
- let (_,_,_,cl) = List.nth dl i in
- let (_,ty) = List.nth cl (j-1) in
- ty
- | _ ->
- raise
- (RefineFailure
- ("Unkown mutual inductive definition " ^ U.string_of_uri uri))
+ 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
+ *)
+ match CicEnvironment.get_obj uri with
+ C.InductiveDefinition (dl,_,_) ->
+ let (_,_,_,cl) = List.nth dl i in
+ let (_,ty) = List.nth cl (j-1) in
+ ty
+ | _ ->
+ 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 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 =
let module C = Cic in
- (* let module R = CicMetaSubst 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
- | C.Appl (C.MutInd (_,_,_)::tl) ->
- let (_,arguments) = split tl left_args_no in
- (n,context,actualtype, arguments@[term]), subst, metasenv
- | 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 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
- | _ -> raise (AssertFailure "Wrong number of arguments"))
- | _ -> raise (AssertFailure "Prod or MutInd expected")
+ match R.whd ~subst context expectedtype with
+ C.MutInd (_,_,_) ->
+ (n,context,actualtype, [term]), subst, metasenv
+ | C.Appl (C.MutInd (_,_,_)::tl) ->
+ let (_,arguments) = split tl left_args_no in
+ (n,context,actualtype, arguments@[term]), subst, metasenv
+ | 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 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
+ | _ -> 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 =
- let module C = Cic in
- let module S = CicSubstitution in
- let module U = UriManager in
- match t with
-(* function *)
- 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.Def (bo,None)) ->
- type_of_aux subst metasenv context (S.lift n bo)
- | 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 ty =
- CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
- in
- ty,subst',metasenv'
- | C.Meta (n,l) ->
- (try
- let (canonical_context, term,ty) = CicUtil.lookup_subst n subst in
- let subst,metasenv =
- check_metasenv_consistency n subst metasenv context
- canonical_context l
- in
- (* trust or check ??? *)
- CicSubstitution.lift_meta l ty, subst, metasenv
- (* 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 =
- check_metasenv_consistency n subst metasenv context
- canonical_context l
- in
- CicSubstitution.lift_meta l ty, subst, metasenv)
- (* 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
- | 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
- in
- (try
- let subst''',metasenv''' =
- fo_unif_subst subst'' context metasenv'' inferredty ty
- in
- ty,subst''',metasenv'''
- 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
- in
- sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
- | C.Lambda (n,s,t) ->
- let sort1,subst',metasenv' = type_of_aux subst metasenv context s 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;
+ let rec type_of_aux subst metasenv context t =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ let module U = UriManager in
+ match t with
+ (* function *)
+ 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.Def (bo,None)) ->
+ type_of_aux subst metasenv context (S.lift n bo)
+ | 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 ty =
+ CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
+ in
+ ty,subst',metasenv'
+ | C.Meta (n,l) ->
+ (try
+ let (canonical_context, term,ty) = CicUtil.lookup_subst n subst in
+ let subst,metasenv =
+ check_metasenv_consistency n subst metasenv context
+ canonical_context l
+ in
+ (* trust or check ??? *)
+ CicSubstitution.lift_meta l ty, subst, metasenv
+ (* 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 =
+ check_metasenv_consistency n subst metasenv context
+ canonical_context l
+ in
+ CicSubstitution.lift_meta l ty, subst, metasenv)
+ (* 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
+ | 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
+ in
+ (try
+ let subst''',metasenv''' =
+ fo_unif_subst subst'' context metasenv'' inferredty ty
+ in
+ ty,subst''',metasenv'''
+ 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
+ in
+ sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
+ | C.Lambda (n,s,t) ->
+ let sort1,subst',metasenv' = type_of_aux subst metasenv context s 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 type2,subst'',metasenv'' =
- type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
- in
- C.Prod (n,s,type2),subst'',metasenv''
- | 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
- 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'
- | C.Appl (he::((_::_) as tl)) ->
- let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
- let tlbody_and_type,subst'',metasenv'' =
- List.fold_right
- (fun x (res,subst,metasenv) ->
- let ty,subst',metasenv' =
- type_of_aux subst metasenv context x
- in
- (x, ty)::res,subst',metasenv'
- ) tl ([],subst',metasenv')
- in
- eat_prods subst'' metasenv'' context hetype tlbody_and_type
- | 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 cty =
- CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
- in
- cty,subst',metasenv'
- | 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)
- in
- cty,subst',metasenv'
- | C.MutConstruct (uri,i,j,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_constr uri i j)
- in
- cty,subst',metasenv'
- | 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 obj =
- try
- CicEnvironment.get_cooked_obj ~trust:true uri
- with Not_found -> assert false
- in
- match obj with
- C.InductiveDefinition (l,expl_params,parsno) ->
- List.nth l i , expl_params, parsno
- | _ ->
- raise
- (RefineFailure
- ("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
- 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 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
- 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))
- 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
- in
- let actual_type = CicReduction.whd ~subst context actual_type in
- let subst,metasenv =
- fo_unif_subst subst context metasenv expected_type actual_type
- in
- (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
- let (_,outtypeinstances,subst,metasenv) =
- List.fold_left
- (fun (j,outtypeinstances,subst,metasenv) p ->
- let constructor =
- if left_args = [] then
- (C.MutConstruct (uri,i,j,exp_named_subst))
+ (CicPp.ppterm sort1)))
+ ) ;
+ let type2,subst'',metasenv'' =
+ type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
+ in
+ C.Prod (n,s,type2),subst'',metasenv''
+ | 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
+ 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'
+ | C.Appl (he::((_::_) as tl)) ->
+ let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
+ let tlbody_and_type,subst'',metasenv'' =
+ List.fold_right
+ (fun x (res,subst,metasenv) ->
+ let ty,subst',metasenv' =
+ type_of_aux subst metasenv context x
+ in
+ (x, ty)::res,subst',metasenv'
+ ) tl ([],subst',metasenv')
+ in
+ eat_prods subst'' metasenv'' context hetype tlbody_and_type
+ | 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 cty =
+ CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
+ in
+ cty,subst',metasenv'
+ | 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)
+ in
+ cty,subst',metasenv'
+ | C.MutConstruct (uri,i,j,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_constr uri i j)
+ in
+ cty,subst',metasenv'
+ | 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 obj =
+ try
+ CicEnvironment.get_cooked_obj ~trust:true uri
+ with Not_found -> assert false
+ in
+ *)
+ match CicEnvironment.get_obj uri with
+ C.InductiveDefinition (l,expl_params,parsno) ->
+ List.nth l i , expl_params, parsno
+ | _ ->
+ raise
+ (RefineFailure
+ ("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
+ 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 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
+ 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.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 =
- 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
- (* 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 *)
+ 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
+ in
+ let actual_type = CicReduction.whd ~subst context actual_type in
+ let subst,metasenv =
+ fo_unif_subst subst context metasenv expected_type actual_type
+ in
+ (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
+ let (_,outtypeinstances,subst,metasenv) =
+ List.fold_left
+ (fun (j,outtypeinstances,subst,metasenv) 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 =
+ 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
+ (* 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 =
- type_of_aux subst metasenv context
- (C.Appl ((outtype :: right_args) @ [term]))
- in
- let (subst,metasenv) =
- List.fold_left
- (fun (subst,metasenv) (constructor_args_no,context,instance,args) ->
- let instance' =
- let appl =
- let outtype' =
- CicSubstitution.lift constructor_args_no outtype
- in
- C.Appl (outtype'::args)
- in
-(*
- (* if appl is not well typed then the type_of below solves the
- * problem *)
- let (_, subst, metasenv) =
- type_of_aux subst metasenv context appl
- in
-*)
- (* DEBUG
- let prova1 = CicMetaSubst.whd subst context appl in
- let prova2 = CicReduction.whd ~subst context appl in
- if not (prova1 = prova2) then
- begin
- prerr_endline ("prova1 =" ^ (CicPp.ppterm prova1));
- prerr_endline ("prova2 =" ^ (CicPp.ppterm prova2));
- end;
- *)
- (* CicMetaSubst.whd subst context appl *)
- CicReduction.whd ~subst context appl
- in
- fo_unif_subst subst context metasenv instance instance')
- (subst,metasenv) outtypeinstances in
- CicReduction.whd ~subst
- context (C.Appl(outtype::right_args@[term])),subst,metasenv
- | C.Fix (i,fl) ->
- let subst,metasenv,types =
- 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
- in
- let len = List.length types in
- let context' = types@context in
- let subst,metasenv =
- List.fold_left
- (fun (subst,metasenv) (name,x,ty,bo) ->
- let ty_of_bo,subst,metasenv =
- type_of_aux subst metasenv context' bo
- in
- fo_unif_subst subst context' metasenv
- ty_of_bo (CicSubstitution.lift len ty)
- ) (subst,metasenv) fl in
- let (_,_,ty,_) = List.nth fl i in
- ty,subst,metasenv
- | C.CoFix (i,fl) ->
- let subst,metasenv,types =
- 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
- in
- let len = List.length types in
- let context' = types@context in
- let subst,metasenv =
- List.fold_left
- (fun (subst,metasenv) (name,ty,bo) ->
- let ty_of_bo,subst,metasenv =
- type_of_aux subst metasenv context' bo
- in
- fo_unif_subst subst context' metasenv
- ty_of_bo (CicSubstitution.lift len ty)
- ) (subst,metasenv) fl in
-
- let (_,ty,_) = List.nth fl i in
- ty,subst,metasenv
+ (* easy case *)
+ let _, subst, metasenv =
+ type_of_aux subst metasenv context
+ (C.Appl ((outtype :: right_args) @ [term]))
+ in
+ let (subst,metasenv) =
+ List.fold_left
+ (fun (subst,metasenv) (constructor_args_no,context,instance,args) ->
+ let instance' =
+ let appl =
+ let outtype' =
+ CicSubstitution.lift constructor_args_no outtype
+ in
+ C.Appl (outtype'::args)
+ in
+ (*
+ (* if appl is not well typed then the type_of below solves the
+ * problem *)
+ let (_, subst, metasenv) =
+ type_of_aux subst metasenv context appl
+ in
+ *)
+ (* DEBUG
+ let prova1 = CicMetaSubst.whd subst context appl in
+ let prova2 = CicReduction.whd ~subst context appl in
+ if not (prova1 = prova2) then
+ begin
+ prerr_endline ("prova1 =" ^ (CicPp.ppterm prova1));
+ prerr_endline ("prova2 =" ^ (CicPp.ppterm prova2));
+ end;
+ *)
+ (* CicMetaSubst.whd subst context appl *)
+ CicReduction.whd ~subst context appl
+ in
+ fo_unif_subst subst context metasenv instance instance')
+ (subst,metasenv) outtypeinstances in
+ CicReduction.whd ~subst
+ context (C.Appl(outtype::right_args@[term])),subst,metasenv
+ | C.Fix (i,fl) ->
+ let subst,metasenv,types =
+ 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
+ in
+ let len = List.length types in
+ let context' = types@context in
+ let subst,metasenv =
+ List.fold_left
+ (fun (subst,metasenv) (name,x,ty,bo) ->
+ let ty_of_bo,subst,metasenv =
+ type_of_aux subst metasenv context' bo
+ in
+ fo_unif_subst subst context' metasenv
+ ty_of_bo (CicSubstitution.lift len ty)
+ ) (subst,metasenv) fl in
+ let (_,_,ty,_) = List.nth fl i in
+ ty,subst,metasenv
+ | C.CoFix (i,fl) ->
+ let subst,metasenv,types =
+ 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
+ in
+ let len = List.length types in
+ let context' = types@context in
+ let subst,metasenv =
+ List.fold_left
+ (fun (subst,metasenv) (name,ty,bo) ->
+ let ty_of_bo,subst,metasenv =
+ type_of_aux subst metasenv context' bo
+ in
+ fo_unif_subst subst context' metasenv
+ ty_of_bo (CicSubstitution.lift len ty)
+ ) (subst,metasenv) fl in
+
+ let (_,ty,_) = List.nth fl i in
+ ty,subst,metasenv
- (* 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
- =
- let module C = Cic in
- let module R = CicReduction in
- let module S = CicSubstitution in
+ (* 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
+ =
+ let module C = Cic in
+ let module R = CicReduction in
+ let module S = CicSubstitution in
let lifted_canonical_context =
- let rec aux i =
- function
- [] -> []
- | (Some (n,C.Decl t))::tl ->
- (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
- | (Some (n,C.Def (t,None)))::tl ->
- (Some (n,C.Def ((S.lift_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 ->
- (Some (n,
- C.Def ((S.lift_meta l (S.lift i t)),
- Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
- in
- aux 1 canonical_context
+ let rec aux i =
+ function
+ [] -> []
+ | (Some (n,C.Decl t))::tl ->
+ (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+ | (Some (n,C.Def (t,None)))::tl ->
+ (Some (n,C.Def ((S.lift_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 ->
+ (Some (n,
+ C.Def ((S.lift_meta l (S.lift i t)),
+ Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
+ in
+ aux 1 canonical_context
in
- try
- List.fold_left2
- (fun (subst,metasenv) t ct ->
- match (t,ct) with
- _,None ->
- subst,metasenv
- | Some t,Some (_,C.Def (ct,_)) ->
- (try
- fo_unif_subst subst context metasenv t ct
- 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
- in
- (try
- fo_unif_subst
- subst' context metasenv' inferredty ct
- 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
- 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)))
+ try
+ List.fold_left2
+ (fun (subst,metasenv) t ct ->
+ match (t,ct) with
+ _,None ->
+ subst,metasenv
+ | Some t,Some (_,C.Def (ct,_)) ->
+ (try
+ fo_unif_subst subst context metasenv t ct
+ 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
+ in
+ (try
+ fo_unif_subst
+ subst' context metasenv' inferredty ct
+ 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
+ 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)))
- and check_exp_named_subst metasubst metasenv context =
- let rec check_exp_named_subst_aux metasubst metasenv substs =
- function
- [] -> metasubst,metasenv
- | ((uri,t) as subst)::tl ->
- let typeofvar =
- CicSubstitution.subst_vars substs (type_of_variable 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 typeoft,metasubst',metasenv' =
- type_of_aux metasubst metasenv context t
- in
- let metasubst'',metasenv'' =
- try
- fo_unif_subst metasubst' context metasenv' typeoft typeofvar
- 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
- in
- check_exp_named_subst_aux metasubst metasenv []
+ and check_exp_named_subst metasubst metasenv context =
+ let rec check_exp_named_subst_aux metasubst metasenv substs =
+ function
+ [] -> metasubst,metasenv
+ | ((uri,t) as subst)::tl ->
+ let typeofvar =
+ CicSubstitution.subst_vars substs (type_of_variable 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 typeoft,metasubst',metasenv' =
+ type_of_aux metasubst metasenv context t
+ in
+ let metasubst'',metasenv'' =
+ try
+ fo_unif_subst metasubst' context metasenv' typeoft typeofvar
+ 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
+ in
+ check_exp_named_subst_aux metasubst metasenv []
- and sort_of_prod subst metasenv context (name,s) (t1, t2) =
- let module C = Cic in
+ and sort_of_prod subst metasenv context (name,s) (t1, t2) =
+ let module C = Cic in
let context_for_t2 = (Some (name,C.Decl s))::context in
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 s2,subst,metasenv
- | (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
- | (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.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 *)
- 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''
- in
- t2'',subst,metasenv
- | (_,_) ->
- 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'')))
+ 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 (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
+ | (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.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 *)
+ 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''
+ in
+ t2'',subst,metasenv
+ | (_,_) ->
+ 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 =
- let rec mk_prod metasenv context =
- function
- [] ->
- 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 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 metasenv
-(* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
- (CicMetaSubst.apply_subst_context subst context)
- Cic.Anonymous
- (CicMetaSubst.apply_subst subst argty)
- in
- (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
- FreshNamesGenerator.mk_fresh_name
- [] context name_hint (Cic.Sort Cic.Prop)
- in
- let metasenv,target =
- mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
- in
- metasenv,Cic.Prod (name,meta,target)
- in
- let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
- let (subst, metasenv) =
- fo_unif_subst subst context metasenv hetype hetype'
- in
- let rec eat_prods metasenv subst context hetype =
+ and eat_prods subst metasenv context hetype tlbody_and_type =
+ let rec mk_prod metasenv context =
function
- [] -> metasenv,subst,hetype
- | (hete, hety)::tl ->
- (match hetype with
- Cic.Prod (n,s,t) ->
- let subst,metasenv =
- fo_unif_subst subst context metasenv hety s
-(*
- 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 *)
+ [] ->
+ 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 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)
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));
- *)
- eat_prods metasenv subst context
- (* (CicMetaSubst.subst subst hete t) tl *)
- (CicSubstitution.subst hete t) tl
- | _ -> assert false
- )
- 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 =
+ mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
+ in
+ metasenv,Cic.Prod (name,meta,target)
+ in
+ let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
+ let (subst, metasenv) =
+ try
+ fo_unif_subst subst context metasenv hetype hetype'
+ with exn ->
+ prerr_endline (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 =
+ function
+ [] -> metasenv,subst,hetype
+ | (hete, hety)::tl ->
+ (match hetype with
+ Cic.Prod (n,s,t) ->
+ let subst,metasenv =
+ try
+ fo_unif_subst subst context metasenv hety s
+ 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 *)
+ 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));
+ *)
+ eat_prods metasenv subst context
+ (* (CicMetaSubst.subst subst hete t) tl *)
+ (CicSubstitution.subst hete t) tl
+ | _ -> assert false
+ )
+ in
let metasenv,subst,t =
- eat_prods metasenv subst context hetype' tlbody_and_type
+ eat_prods metasenv subst context hetype' tlbody_and_type
in
- t,subst,metasenv
-(*
- let rec aux context' args (resty,subst,metasenv) =
- function
- [] -> resty,subst,metasenv
- | (arg,argty)::tl ->
- let args' =
- List.map
- (function
- None -> assert false
- | Some t -> Some (CicMetaSubst.lift subst 1 t)
- ) args in
- let argty' = CicMetaSubst.lift subst (List.length args) argty in
- let name =
- (* The name must be fresh for (context'@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 =
- FreshNamesGenerator.mk_fresh_name
- (CicMetaSubst.apply_subst_metasenv subst metasenv)
- (CicMetaSubst.apply_subst_context subst context)
- Cic.Anonymous
- (CicMetaSubst.apply_subst subst argty)
- in
- (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
- FreshNamesGenerator.mk_fresh_name
- [] (context'@context) name_hint (Cic.Sort Cic.Prop)
- in
- let context'' = Some (name, Cic.Decl argty') :: context' in
- let (metasenv, idx) =
- CicMkImplicit.mk_implicit_type metasenv (context'' @ context) in
- let irl =
- (Some (Cic.Rel 1))::args' @
- (CicMkImplicit.identity_relocation_list_for_metavariable ~start:2
- context)
- in
- let newmeta = Cic.Meta (idx, irl) in
- let prod = Cic.Prod (name, argty, newmeta) in
- let (_, subst, metasenv) = type_of_aux subst metasenv context prod in
- let (subst, metasenv) =
- fo_unif_subst subst context metasenv resty prod
- in
- aux context'' (Some arg :: args)
- (CicMetaSubst.subst subst arg newmeta, subst, metasenv) tl
+ t,subst,metasenv
+ (* eat prods ends here! *)
in
- aux [] [] (hetype,subst,metasenv) tlbody_and_type
-*)
- in
let ty,subst',metasenv' =
- type_of_aux [] metasenv context t
+ type_of_aux [] metasenv context 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
-e' sempre istanziato *)
- let substituted_metasenv =
- CicMetaSubst.apply_subst_metasenv subst' metasenv' in
- (* metasenv' *)
-(* substituted_t,substituted_ty,substituted_metasenv *)
-(* ANDREA: spostare tutta questa robaccia da un altra parte *)
- let cleaned_t =
- FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
- let cleaned_ty =
- FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
- let cleaned_metasenv =
- List.map
+ 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
+ e' sempre istanziato *)
+ let substituted_metasenv =
+ CicMetaSubst.apply_subst_metasenv subst' metasenv' in
+ (* metasenv' *)
+ (* substituted_t,substituted_ty,substituted_metasenv *)
+ (* ANDREA: spostare tutta questa robaccia da un altra parte *)
+ let cleaned_t =
+ FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
+ let cleaned_ty =
+ FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
+ let cleaned_metasenv =
+ List.map
(function (n,context,ty) ->
- let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
- 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' =
- match ty with
- None -> None
- | Some ty ->
- Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
- in
- Some (n, Cic.Def (bo',ty'))
- ) context
- in
- (n,context',ty')
+ let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
+ 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' =
+ match ty with
+ None -> None
+ | Some ty ->
+ Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
+ in
+ Some (n, Cic.Def (bo',ty'))
+ ) context
+ in
+ (n,context',ty')
) substituted_metasenv
- in
- (cleaned_t,cleaned_ty,cleaned_metasenv)
+ in
+ (cleaned_t,cleaned_ty,cleaned_metasenv)
;;
projects / helm.git / commitdiff