in
aux 1 context
-let interpretate_term
- ?(create_dummy_ids=false) ~mk_choice ~context ~env ~uri ~is_path ast
- ~localization_tbl
+let interpretate_term_and_interpretate_term_option
+ ?(create_dummy_ids=false)
+ ~obj_context ~mk_choice ~env ~uri ~is_path ~localization_tbl
=
(* create_dummy_ids shouldbe used only for interpretating patterns *)
assert (uri = None);
in
let cic_body = aux ~localize loc (cic_name :: context) body in
NCic.LetIn (cic_name, cic_typ, cic_def, cic_body)
- | CicNotationPt.LetRec (_kind, _defs, _body) ->
- assert false (*
- let context' =
- List.fold_left
- (fun acc (_, (name, _), _, _) ->
- cic_name_of_name name :: acc)
- context defs
- in
- let cic_body =
- let unlocalized_body = aux ~localize:false loc context' body in
- match unlocalized_body with
- NCic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n
- | NCic.Appl (NCic.Rel n::l) when n <= List.length defs ->
- (try
- let l' =
- List.map
- (function t ->
- let t',subst,metasenv =
- CicMetaSubst.delift_rels [] [] (List.length defs) t
- in
- assert (subst=[]);
- assert (metasenv=[]);
- t') l
- in
- (* We can avoid the LetIn. But maybe we need to recompute l'
- so that it is localized *)
- if localize then
- match body with
- CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
- (* since we avoid the letin, the context has no
- * recfuns in it *)
- let l' = List.map (aux ~localize loc context) l in
- `AvoidLetIn (n,l')
- | _ -> assert false
- else
- `AvoidLetIn (n,l')
- with
- CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
- if localize then
- `AddLetIn (aux ~localize loc context' body)
- else
- `AddLetIn unlocalized_body)
- | _ ->
- if localize then
- `AddLetIn (aux ~localize loc context' body)
- else
- `AddLetIn unlocalized_body
- in
- let inductiveFuns =
- List.map
- (fun (params, (name, typ), body, decr_idx) ->
- let add_binders kind t =
- List.fold_right
- (fun var t -> CicNotationPt.Binder (kind, var, t)) params t
- in
- let cic_body =
- aux ~localize loc context' (add_binders `Lambda body) in
- let cic_type =
- aux_option ~localize loc context (Some `Type)
- (HExtlib.map_option (add_binders `Pi) typ) in
- let name =
- match cic_name_of_name name with
- | NCic.Anonymous ->
- CicNotationPt.fail loc
- "Recursive functions cannot be anonymous"
- | NCic.Name name -> name
- in
- (name, decr_idx, cic_type, cic_body))
- defs
- in
- let fix_or_cofix n =
- match kind with
- `Inductive -> NCic.Fix (n,inductiveFuns)
- | `CoInductive ->
- let coinductiveFuns =
- List.map
- (fun (name, _, typ, body) -> name, typ, body)
- inductiveFuns
- in
- NCic.CoFix (n,coinductiveFuns)
- in
- let counter = ref ~-1 in
- let build_term _ (var,_,ty,_) t =
- incr counter;
- NCic.LetIn (NCic.Name var, fix_or_cofix !counter, ty, t)
- in
- (match cic_body with
- `AvoidLetInNoAppl n ->
- let n' = List.length inductiveFuns - n in
- fix_or_cofix n'
- | `AvoidLetIn (n,l) ->
- let n' = List.length inductiveFuns - n in
- NCic.Appl (fix_or_cofix n'::l)
- | `AddLetIn cic_body ->
- List.fold_right (build_term inductiveFuns) inductiveFuns
- cic_body)
-*)
+ | CicNotationPt.LetRec (_kind, _defs, _body) -> assert false
| CicNotationPt.Ident _
| CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed
| CicNotationPt.Ident (name, subst) ->
(try
NCic.Rel (find_in_context name context)
with Not_found ->
- Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
+ try NCic.Const (List.assoc name obj_context)
+ with Not_found ->
+ Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
| CicNotationPt.Uri (name, subst) ->
assert (subst = None);
(try
| Some CicNotationPt.Implicit -> NCic.Implicit annotation
| Some term -> aux ~localize loc context term
in
- aux ~localize:true HExtlib.dummy_floc context ast
+ (fun ~context -> aux ~localize:true HExtlib.dummy_floc context),
+ (fun ~context -> aux_option ~localize:true HExtlib.dummy_floc context)
+;;
let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
- ~localization_tbl
+ ~obj_context ~localization_tbl ~mk_choice
+=
+ let context = List.map fst context in
+ fst
+ (interpretate_term_and_interpretate_term_option
+ ~obj_context ~mk_choice ~create_dummy_ids ~env ~uri ~is_path ~localization_tbl)
+ ~context ast
+;;
+
+let interpretate_term_option
+ ?(create_dummy_ids=false) ~context ~env ~uri ~is_path
+ ~localization_tbl ~mk_choice ~obj_context
=
let context = List.map fst context in
- interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast
-~localization_tbl
+ snd
+ (interpretate_term_and_interpretate_term_option
+ ~obj_context ~mk_choice ~create_dummy_ids ~env ~uri ~is_path ~localization_tbl)
+ ~context
+;;
+
+let new_flavour_of_flavour = function
+ | `Definition -> `Definition
+ | `MutualDefinition -> `Definition
+ | `Fact -> `Fact
+ | `Lemma -> `Lemma
+ | `Remark -> `Corollary
+ | `Theorem -> `Theorem
+ | `Variant -> `Corollary
+ | `Axiom -> `Fact
;;
+(*
+let interpretate_obj ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
+ ~localization_tbl
+=
+ assert (context = []);
+ assert (is_path = false);
+ let interpretate_term ?(obj_context=[]) =
+ interpretate_term ~mk_choice ~localization_tbl ~obj_context in
+ let interpretate_term_option ?(obj_context=[]) =
+ interpretate_term_option ~mk_choice ~localization_tbl ~obj_context in
+ match obj with
+ | CicNotationPt.Theorem (flavour, name, ty, bo) ->
+ let attrs = `Provided, new_flavour_of_flavour flavour in
+ let ty' = interpretate_term [] env None false ty in
+ let height = (* XXX calculate *) 0 in
+ uri, height, [], [],
+ (match bo,flavour with
+ None,`Axiom ->
+ NCic.Constant (name,None,ty',attrs)
+ | Some bo,`Axiom -> assert false
+ | None,_ ->
+ NCic.Constant (name,NCic.Implicit None,ty',attrs)
+ | Some bo,_ ->
+ match bo with
+ | CicNotationPt.LetRec (kind, defs, _) ->
+ let inductive = kind = `Inductive in
+ let obj_context =
+ List.split
+ (List.fold_left
+ (fun (i,acc) (_,(name,_),_,k) ->
+ ((name, NReference.reference_of_spec uri
+ (if inductive then NReference.Fix (i,k,0)
+ else NReference.CoFix i)) :: acc)
+ (0,[]) defs))
+ in
+ let inductiveFuns =
+ List.map
+ (fun (params, (name, typ), body, decr_idx) ->
+ let add_binders kind t =
+ List.fold_right
+ (fun var t ->
+ CicNotationPt.Binder (kind, var, t)) params t
+ in
+ let cic_body =
+ interpretate_term ~context ~env ~uri:None ~is_path:false
+ (add_binders `Lambda body)
+ in
+ let cic_type =
+ interpretate_term_option ~context ~env ~uri:None
+ ~is_path:false `Type
+ (HExtlib.map_option (add_binders `Pi) typ)
+ in
+ (name, decr_idx, cic_type, cic_body))
+ defs
+ in
+ NCic.Fixpoint (inductive,inductiveFuns,attrs)
+ | bo ->
+ let bo =
+ interpretate_term ~context:[] ~env ~uri:None ~is_path:false bo
+ in
+ NCic.Constant (name,Some bo,ty',attrs))
+ | _ -> assert false
+(*
+ | CicNotationPt.Inductive (params,tyl) ->
+ let uri = match uri with Some uri -> uri | None -> assert false in
+ let context,params =
+ let context,res =
+ List.fold_left
+ (fun (context,res) (name,t) ->
+ let t =
+ match t with
+ None -> CicNotationPt.Implicit
+ | Some t -> t in
+ let name = CicNotationUtil.cic_name_of_name name in
+ name::context,(name, interpretate_term context env None false t)::res
+ ) ([],[]) params
+ in
+ context,List.rev res in
+ let add_params =
+ List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
+ let obj_context =
+ snd (
+ List.fold_left
+ (*here the explicit_named_substituion is assumed to be of length 0 *)
+ (fun (i,res) (name,_,_,_) -> i + 1,(name,Cic.MutInd (uri,i,[]))::res)
+ (0,[]) tyl) in
+ let tyl =
+ List.map
+ (fun (name,b,ty,cl) ->
+ let ty' = add_params (interpretate_term context env None false ty) in
+ let cl' =
+ List.map
+ (fun (name,ty) ->
+ let ty' =
+ add_params
+ (interpretate_term ~obj_context ~context ~env ~uri:None
+ ~is_path:false ty)
+ in
+ name,ty'
+ ) cl
+ in
+ name,b,ty',cl'
+ ) tyl
+ in
+ Cic.InductiveDefinition (tyl,[],List.length params,[])
+ | CicNotationPt.Record (params,name,ty,fields) ->
+ let uri = match uri with Some uri -> uri | None -> assert false in
+ let context,params =
+ let context,res =
+ List.fold_left
+ (fun (context,res) (name,t) ->
+ let t =
+ match t with
+ None -> CicNotationPt.Implicit
+ | Some t -> t in
+ let name = CicNotationUtil.cic_name_of_name name in
+ name::context,(name, interpretate_term context env None false t)::res
+ ) ([],[]) params
+ in
+ context,List.rev res in
+ let add_params =
+ List.fold_right
+ (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
+ let ty' = add_params (interpretate_term context env None false ty) in
+ let fields' =
+ snd (
+ List.fold_left
+ (fun (context,res) (name,ty,_coercion,arity) ->
+ let context' = Cic.Name name :: context in
+ context',(name,interpretate_term context env None false ty)::res
+ ) (context,[]) fields) in
+ let concl =
+ (*here the explicit_named_substituion is assumed to be of length 0 *)
+ let mutind = Cic.MutInd (uri,0,[]) in
+ if params = [] then mutind
+ else
+ Cic.Appl
+ (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in
+ let con =
+ List.fold_left
+ (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t))
+ concl fields' in
+ let con' = add_params con in
+ let tyl = [name,true,ty',["mk_" ^ name,con']] in
+ let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
+ Cic.InductiveDefinition
+ (tyl,[],List.length params,[`Class (`Record field_names)])
+*)
+;;
+*)
+
let disambiguate_term ~context ~metasenv ~subst ?goal
~mk_implicit ~description_of_alias ~mk_choice
~aliases ~universe ~coercion_db ~lookup_in_library
~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
~passes:(MultiPassDisambiguator.passes ())
~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term
- ~interpretate_thing:(interpretate_term ~mk_choice (?create_dummy_ids:None))
+ ~interpretate_thing:(interpretate_term ~obj_context:[] ~mk_choice (?create_dummy_ids:None))
~refine_thing:(refine_term ~coercion_db) (text,prefix_len,term)
~mk_localization_tbl ~hint ~subst
in
aux metasenv subst [] he ty_he args
(*D*)in outside(); rc with exc -> outside (); raise exc
;;
+
+let rec first f l1 l2 =
+ match l1,l2 with
+ | x1::tl1, x2::tl2 ->
+ (try f x1 x2 with Not_found -> first f tl1 tl2)
+ | _ -> raise Not_found
+;;
+
+let rec find add dt t =
+ if dt == add then t
+ else
+ let dl, l =
+ match dt, t with
+ | C.Meta (_,(_,C.Ctx dl)), C.Meta (_,(_,C.Ctx l))
+ | C.Appl dl,C.Appl l -> dl,l
+ | C.Lambda (_,ds,dt), C.Lambda (_,s,t)
+ | C.Prod (_,ds,dt), C.Prod (_,s,t) -> [ds;dt],[s;t]
+ | C.LetIn (_,ds,db,dt), C.LetIn (_,s,b,t) -> [ds;db;dt],[s;b;t]
+ | C.Match (_,dot,dt,dl), C.Match (_,ot,t,l) -> (dot::dt::dl),(ot::t::l)
+ | _ -> raise Not_found
+ in
+ first (find add) dl l
+;;
+
+let relocalise old_localise dt t add =
+ old_localise
+ (try find add dt t with Not_found -> assert false)
+;;
+
+let undebruijnate inductive ref t rev_fl =
+ NCicSubstitution.psubst (fun x -> x)
+ (HExtlib.list_mapi
+ (fun (_,_,rno,_,_,_) i ->
+ NCic.Const
+ (if inductive then NReference.mk_fix i rno ref
+ else NReference.mk_cofix i ref))
+ rev_fl)
+ t
+;;
+
+
+let typeof_obj hdb
+ ?(localise=fun _ -> Stdpp.dummy_loc)
+ ~look_for_coercion (uri,height,metasenv,subst, obj)
+=
+ let check_type metasenv subst (ty as orig_ty) = (* XXX fattorizza *)
+ let metasenv, subst, ty, sort =
+ typeof hdb ~localise ~look_for_coercion metasenv subst [] ty None
+ in
+ let metasenv, subst, ty, _ =
+ force_to_sort hdb ~look_for_coercion
+ metasenv subst [] ty orig_ty localise sort
+ in
+ metasenv, subst, ty
+ in
+ match obj with
+ | C.Constant (relevance, name, bo, ty , attr) ->
+ let metasenv, subst, ty = check_type metasenv subst ty in
+ let metasenv, subst, bo, ty, height =
+ match bo with
+ | Some bo ->
+ let metasenv, subst, bo, ty =
+ typeof hdb ~localise ~look_for_coercion
+ metasenv subst [] bo (Some ty)
+ in
+ let height = (* XXX recalculate *) height in
+ metasenv, subst, Some bo, ty, height
+ | None -> metasenv, subst, None, ty, 0
+ in
+ uri, height, metasenv, subst,
+ C.Constant (relevance, name, bo, ty, attr)
+ | C.Fixpoint (inductive, fl, attr) ->
+ let len = List.length fl in
+ let types, metasenv, subst, rev_fl =
+ List.fold_left
+ (fun (types, metasenv, subst, fl) (relevance,name,k,ty,bo) ->
+ let metasenv, subst, ty = check_type metasenv subst ty in
+ let dbo = NCicTypeChecker.debruijn uri len [] bo in
+ let localise = relocalise localise dbo bo in
+ (name,C.Decl ty)::types,
+ metasenv, subst, (relevance,name,k,ty,dbo,localise)::fl
+ ) ([], metasenv, subst, []) fl (* XXX kl rimosso nel nucleo *)
+ in
+ let metasenv, subst, fl =
+ List.fold_left
+ (fun (metasenv,subst,fl) (relevance,name,k,ty,dbo,localise) ->
+ let metasenv, subst, dbo, ty =
+ typeof hdb ~localise ~look_for_coercion
+ metasenv subst types dbo (Some ty)
+ in
+ metasenv, subst, (relevance,name,k,ty,dbo)::fl)
+ (metasenv, subst, []) rev_fl
+ in
+ let height = (* XXX recalculate *) height in
+ let fl =
+ List.map
+ (fun (relevance,name,k,ty,dbo) ->
+ let bo =
+ undebruijnate inductive
+ (NReference.reference_of_spec uri
+ (if inductive then NReference.Fix (0,k,0)
+ else NReference.CoFix 0)) dbo rev_fl
+ in
+ relevance,name,k,ty,bo)
+ fl
+ in
+ uri, height, metasenv, subst,
+ C.Fixpoint (inductive, fl, attr)
+
+ | C.Inductive (ind, leftno, itl, attr) -> assert false
+(*
+ (* let's check if the arity of the inductive types are well formed *)
+ List.iter (fun (_,_,x,_) -> ignore (typeof ~subst ~metasenv [] x)) tyl;
+ (* let's check if the types of the inductive constructors are well formed. *)
+ let len = List.length tyl in
+ let tys = List.rev_map (fun (_,n,ty,_) -> (n,(C.Decl ty))) tyl in
+ ignore
+ (List.fold_right
+ (fun (it_relev,_,ty,cl) i ->
+ let context,ty_sort = split_prods ~subst [] ~-1 ty in
+ let sx_context_ty_rev,_ = HExtlib.split_nth leftno (List.rev context) in
+ List.iter
+ (fun (k_relev,_,te) ->
+ let _,k_relev = HExtlib.split_nth leftno k_relev in
+ let te = debruijn uri len [] te in
+ let context,te = split_prods ~subst tys leftno te in
+ let _,chopped_context_rev =
+ HExtlib.split_nth (List.length tys) (List.rev context) in
+ let sx_context_te_rev,_ =
+ HExtlib.split_nth leftno chopped_context_rev in
+ (try
+ ignore (List.fold_left2
+ (fun context item1 item2 ->
+ let convertible =
+ match item1,item2 with
+ (n1,C.Decl ty1),(n2,C.Decl ty2) ->
+ n1 = n2 &&
+ R.are_convertible ~metasenv ~subst context ty1 ty2
+ | (n1,C.Def (bo1,ty1)),(n2,C.Def (bo2,ty2)) ->
+ n1 = n2
+ && R.are_convertible ~metasenv ~subst context ty1 ty2
+ && R.are_convertible ~metasenv ~subst context bo1 bo2
+ | _,_ -> false
+ in
+ if not convertible then
+ raise (TypeCheckerFailure (lazy
+ ("Mismatch between the left parameters of the constructor " ^
+ "and those of its inductive type")))
+ else
+ item1::context
+ ) [] sx_context_ty_rev sx_context_te_rev)
+ with Invalid_argument "List.fold_left2" -> assert false);
+ let con_sort = typeof ~subst ~metasenv context te in
+ (match R.whd ~subst context con_sort, R.whd ~subst [] ty_sort with
+ (C.Sort (C.Type u1) as s1), (C.Sort (C.Type u2) as s2) ->
+ if not (E.universe_leq u1 u2) then
+ raise
+ (TypeCheckerFailure
+ (lazy ("The type " ^ PP.ppterm ~metasenv ~subst ~context s1^
+ " of the constructor is not included in the inductive" ^
+ " type sort " ^ PP.ppterm ~metasenv ~subst ~context s2)))
+ | C.Sort _, C.Sort C.Prop
+ | C.Sort _, C.Sort C.Type _ -> ()
+ | _, _ ->
+ raise
+ (TypeCheckerFailure
+ (lazy ("Wrong constructor or inductive arity shape"))));
+ (* let's check also the positivity conditions *)
+ if
+ not
+ (are_all_occurrences_positive ~subst context uri leftno
+ (i+leftno) leftno (len+leftno) te)
+ then
+ raise
+ (TypeCheckerFailure
+ (lazy ("Non positive occurence in "^NUri.string_of_uri
+ uri)))
+ else check_relevance ~subst ~metasenv context k_relev te)
+ cl;
+ check_relevance ~subst ~metasenv [] it_relev ty;
+ i+1)
+ tyl 1)
+*)
+
+
+;;
+
+
+
(* vim:set foldmethod=marker: *)
projects / helm.git / commitdiff