-let domain_of_term ~context ast =
- (* "aux" keeps domain in reverse order and doesn't care about duplicates.
- * Domain item more in deep in the list will be processed first.
- *)
- let rec aux loc context = function
- | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
- | CicAst.AttributedTerm (_, term) -> aux loc context term
- | CicAst.Appl terms ->
- List.fold_left (fun dom term -> aux loc context term @ dom) [] terms
- | CicAst.Binder (kind, (var, typ), body) ->
- let kind_dom =
- match kind with
- | `Exists -> [ Symbol ("exists", 0) ]
- | _ -> []
- in
- let type_dom = aux_option loc context typ in
- let body_dom = aux loc (var :: context) body in
- body_dom @ type_dom @ kind_dom
- | CicAst.Case (term, indty_ident, outtype, branches) ->
- let term_dom = aux loc context term in
- let outtype_dom = aux_option loc context outtype in
- let do_branch ((head, args), term) =
- let (term_context, args_domain) =
- List.fold_left
- (fun (cont, dom) (name, typ) ->
- (name :: cont,
- (match typ with
- | None -> dom
- | Some typ -> aux loc cont typ @ dom)))
- (context, []) args
- in
- args_domain @ aux loc term_context term
- in
- let branches_dom =
- List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches
- in
- branches_dom @ outtype_dom @ term_dom @
- (match indty_ident with None -> [] | Some ident -> [ Id ident ])
- | CicAst.LetIn ((var, typ), body, where) ->
- let body_dom = aux loc context body in
- let type_dom = aux_option loc context typ in
- let where_dom = aux loc (var :: context) where in
- where_dom @ type_dom @ body_dom
- | CicAst.LetRec (kind, defs, where) ->
- let context' =
- List.fold_left (fun acc ((var, typ), _, _) -> var :: acc)
- context defs
- in
- let where_dom = aux loc context' where in
- let defs_dom =
- List.fold_left
- (fun dom ((_, typ), body, _) ->
- aux loc context' body @ aux_option loc context typ)
- [] defs
- in
- where_dom @ defs_dom
- | CicAst.Ident (name, subst) ->
- (try
- let index = find_in_environment name context in
- if subst <> None then
- CicTextualParser2.fail loc
- "Explicit substitutions not allowed here"
- else
- []
- with Not_found ->
- (match subst with
- | None -> [Id name]
- | Some subst ->
- List.fold_left
- (fun dom (_, term) ->
- let dom' = aux loc context term in
- dom' @ dom)
- [Id name] subst))
- | CicAst.Uri _ -> []
- | CicAst.Implicit -> []
- | CicAst.Num (num, i) -> [ Num i ]
- | CicAst.Meta (index, local_context) ->
- List.fold_left (fun dom term -> aux_option loc context term @ dom) []
- local_context
- | CicAst.Sort _ -> []
- | CicAst.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ]
- | CicAst.UserInput -> assert false
-
- and aux_option loc context = function
- | None -> []
- | Some t -> aux loc context t
- in
+let interpretate_path ~context ~env path =
+ interpretate_term ~context ~env ~uri:None ~is_path:true path
+
+let interpretate_obj ~context ~env ~uri ~is_path obj =
+ assert (context = []);
+ assert (is_path = false);
+ match obj with
+ | GrafiteAst.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) ->
+ Cic.Name 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 (Cic.Name name,ty,t)) params in
+ let name_to_uris =
+ snd (
+ List.fold_left
+ (*here the explicit_named_substituion is assumed to be of length 0 *)
+ (fun (i,res) (name,_,_,_) ->
+ i + 1,(name,name,Cic.MutInd (uri,i,[]))::res
+ ) (0,[]) tyl) in
+ let con_env = DisambiguateTypes.env_of_list name_to_uris env 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
+ ) tyl (List.length tyl - 1,t)) 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 context con_env None false ty)
+ in
+ name,undebrujin ty'
+ ) cl
+ in
+ name,b,ty',cl'
+ ) tyl
+ in
+ Cic.InductiveDefinition (tyl,[],List.length params,[])
+ | GrafiteAst.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) ->
+ (Cic.Name 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 (Cic.Name 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) ->
+ 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 fst fields in
+ Cic.InductiveDefinition
+ (tyl,[],List.length params,[`Class (`Record field_names)])
+ | GrafiteAst.Theorem (flavour, name, ty, bo) ->
+ let attrs = [`Flavour flavour] in
+ let ty' = interpretate_term [] env None false ty in
+ (match bo with
+ None ->
+ Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
+ | Some bo ->
+ let bo' = Some (interpretate_term [] env None false bo) in
+ Cic.Constant (name,bo',ty',[],attrs))
+