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
projects / helm.git / blobdiff