-let domain_of_term ~context ast =
- let rec aux loc context = function
- | CicTextualParser2Ast.LocatedTerm (_, term) -> aux loc context term
- | CicTextualParser2Ast.Appl terms ->
- List.fold_left (fun dom term -> Domain.union dom (aux loc context term))
- Domain.empty terms
- | CicTextualParser2Ast.Appl_symbol (symb, i, args) ->
- List.fold_left (fun dom term -> Domain.union dom (aux loc context term))
- (Domain.singleton (Symbol (symb, i))) args
- | CicTextualParser2Ast.Binder (_, var, typ, body) ->
- let type_dom = aux_option loc context typ in
- let body_dom = aux loc (var :: context) body in
- Domain.union type_dom body_dom
- | CicTextualParser2Ast.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 (pat, term) =
- match pat with
- | _ :: tl ->
- aux loc
- (List.fold_left (fun acc var -> (Cic.Name var) :: acc)
- context tl)
- term
- | [] -> assert false
- in
- let branches_dom =
- List.fold_left (fun dom branch -> Domain.union dom (do_branch branch))
- Domain.empty branches
- in
- Domain.add (Id indty_ident)
- (Domain.union outtype_dom (Domain.union term_dom branches_dom))
- | CicTextualParser2Ast.LetIn (var, body, where) ->
- let body_dom = aux loc context body in
- let where_dom = aux loc (Cic.Name var :: context) where in
- Domain.union body_dom where_dom
- | CicTextualParser2Ast.LetRec (kind, defs, where) ->
- let context' =
- List.fold_left (fun acc (var, _, _, _) -> Cic.Name var :: acc)
- context defs
- in
- let where_dom = aux loc context' where in
- let defs_dom =
+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
+ | TacticAst.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,[])
+ | TacticAst.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)])
+ | TacticAst.Theorem (_,name,ty,bo) ->
+ let ty' = interpretate_term [] env None false ty in
+ match bo with
+ None ->
+ Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],[])
+ | Some bo ->
+ let bo' = Some (interpretate_term [] env None false bo) in
+ Cic.Constant (name,bo',ty',[],[])
+
+ (* e.g. [5;1;1;1;2;3;4;1;2] -> [2;1;4;3;5] *)
+let rev_uniq =
+ let module SortedItem =
+ struct
+ type t = DisambiguateTypes.domain_item
+ let compare = Pervasives.compare
+ end
+ in
+ let module Set = Set.Make (SortedItem) in
+ fun l ->
+ let rev_l = List.rev l in
+ let (_, uniq_rev_l) =
+ List.fold_left
+ (fun (members, rev_l) elt ->
+ if Set.mem elt members then
+ (members, rev_l)
+ else
+ Set.add elt members, elt :: rev_l)
+ (Set.empty, []) rev_l
+ in
+ List.rev uniq_rev_l
+
+(* "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 domain_rev_of_term ?(loc = CicAst.dummy_floc) context = function
+ | CicAst.AttributedTerm (`Loc loc, term) ->
+ domain_rev_of_term ~loc context term
+ | CicAst.AttributedTerm (_, term) -> domain_rev_of_term ~loc context term
+ | CicAst.Appl terms ->
+ List.fold_left
+ (fun dom term -> domain_rev_of_term ~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 = domain_rev_of_term_option loc context typ in
+ let body_dom = domain_rev_of_term ~loc (var :: context) body in
+ body_dom @ type_dom @ kind_dom
+ | CicAst.Case (term, indty_ident, outtype, branches) ->
+ let term_dom = domain_rev_of_term ~loc context term in
+ let outtype_dom = domain_rev_of_term_option loc context outtype in
+ let get_first_constructor = function
+ | [] -> []
+ | ((head, _), _) :: _ -> [ Id head ]
+ in
+ let do_branch ((head, args), term) =
+ let (term_context, args_domain) =