interp_db <- Some (initial_db self)
end
-let idref register_ref =
- let id = ref 0 in
- fun ?reference t ->
- incr id;
- let id = "i" ^ string_of_int !id in
- (match reference with None -> () | Some r -> register_ref id r);
- Ast.AttributedTerm (`IdRef id, t)
-;;
-
let level_of_uri u =
let name = NUri.name_of_uri u in
assert(String.length name > String.length "Type");
let find_level2_patterns32 status pid =
IntMap.find pid status#interp_db.level2_patterns32
-let add_idrefs =
- List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t))
-
-let instantiate32 idrefs env symbol args =
+let instantiate32 env symbol args =
let rec instantiate_arg = function
| Ast.IdentArg (n, name) ->
let t =
in
add_lambda t (n - count_lambda t)
in
- let head =
- let symbol = Ast.Symbol (symbol, None) in
- add_idrefs idrefs symbol
- in
+ let head = Ast.Symbol (symbol, None) in
if args = [] then head
else Ast.Appl (head :: List.map instantiate_arg args)
let fresh_id status =
- let counter = status#interp_db.counter+1 in
- status#set_interp_db ({ status#interp_db with counter = counter }), counter
+ let counter = status#interp_db.counter + 1 in
+ status#set_interp_db {status#interp_db with counter = counter},counter
let load_patterns32 status t =
let t =
in
aux 0
-(* CODICE c&p da NCicPp *)
let nast_of_cic0 status
- ~(idref:
- ?reference:NReference.reference -> NotationPt.term -> NotationPt.term)
~output_type ~metasenv ~subst k ~context =
function
| NCic.Rel n ->
(try
let name,_ = List.nth context (n-1) in
let name = if name = "_" then "__"^string_of_int n else name in
- idref (Ast.Ident (name,`Ambiguous))
+ Ast.Ident (name,`Ambiguous)
with Failure "nth" | Invalid_argument "List.nth" ->
- idref (Ast.Ident ("-" ^ string_of_int (n - List.length
- context),`Ambiguous)))
- | NCic.Const r -> idref ~reference:r (Ast.Ident (NCicPp.r2s status true r, `Ambiguous))
+ Ast.Ident ("-" ^ string_of_int (n - List.length context),`Ambiguous))
+ | NCic.Const r ->
+ let uri = `Uri (NReference.string_of_reference r) in
+ Ast.Ident (NCicPp.r2s status true r, uri)
| NCic.Meta (n,lc) when List.mem_assoc n subst ->
let _,_,t,_ = List.assoc n subst in
k ~context (NCicSubstitution.subst_meta status lc t)
| NCic.Meta (n,(s,l)) ->
(* CSC: qua non dovremmo espandere *)
let l = NCicUtils.expand_local_context l in
- idref (Ast.Meta
- (n, List.map (fun x -> Some (k ~context (NCicSubstitution.lift status s x))) l))
- | NCic.Sort NCic.Prop -> idref (Ast.Sort `Prop)
- | NCic.Sort NCic.Type [] -> idref (Ast.Sort `Set)
+ Ast.Meta
+ (n, List.map (fun x -> Some (k ~context (NCicSubstitution.lift status s x))) l)
+ | NCic.Sort NCic.Prop -> Ast.Sort `Prop
+ | NCic.Sort NCic.Type [] -> Ast.Sort `Set
| NCic.Sort NCic.Type ((`Type,u)::_) ->
- idref(Ast.Sort (`NType (level_of_uri u)))
+ Ast.Sort (`NType (level_of_uri u))
| NCic.Sort NCic.Type ((`CProp,u)::_) ->
- idref(Ast.Sort (`NCProp (level_of_uri u)))
+ Ast.Sort (`NCProp (level_of_uri u))
| NCic.Sort NCic.Type ((`Succ,u)::_) ->
- idref(Ast.Sort (`NType (level_of_uri u ^ "+1")))
- | NCic.Implicit `Hole -> idref (Ast.UserInput)
- | NCic.Implicit `Vector -> idref (Ast.Implicit `Vector)
- | NCic.Implicit _ -> idref (Ast.Implicit `JustOne)
+ Ast.Sort (`NType (level_of_uri u ^ "+1"))
+ | NCic.Implicit `Hole -> Ast.UserInput
+ | NCic.Implicit `Vector -> Ast.Implicit `Vector
+ | NCic.Implicit _ -> Ast.Implicit `JustOne
| NCic.Prod (n,s,t) ->
let n = if n.[0] = '_' then "_" else n in
let binder_kind = `Forall in
- idref (Ast.Binder (binder_kind, (Ast.Ident (n,`Ambiguous), Some (k ~context s)),
- k ~context:((n,NCic.Decl s)::context) t))
+ Ast.Binder (binder_kind, (Ast.Ident (n,`Ambiguous), Some (k ~context s)),
+ k ~context:((n,NCic.Decl s)::context) t)
| NCic.Lambda (n,s,t) ->
- idref (Ast.Binder (`Lambda,(Ast.Ident (n,`Ambiguous), Some (k ~context s)),
- k ~context:((n,NCic.Decl s)::context) t))
+ Ast.Binder (`Lambda,(Ast.Ident (n,`Ambiguous), Some (k ~context s)),
+ k ~context:((n,NCic.Decl s)::context) t)
| NCic.LetIn (n,s,ty,NCic.Rel 1) ->
- idref (Ast.Cast (k ~context ty, k ~context s))
+ Ast.Cast (k ~context ty, k ~context s)
| NCic.LetIn (n,s,ty,t) ->
- idref (Ast.LetIn ((Ast.Ident (n,`Ambiguous), Some (k ~context s)), k ~context
- ty, k ~context:((n,NCic.Decl s)::context) t))
+ Ast.LetIn ((Ast.Ident (n,`Ambiguous), Some (k ~context s)), k ~context
+ ty, k ~context:((n,NCic.Decl s)::context) t)
| NCic.Appl (NCic.Meta (n,lc) :: args) when List.mem_assoc n subst ->
let _,_,t,_ = List.assoc n subst in
let hd = NCicSubstitution.subst_meta status lc t in
| _ -> NCic.Appl (hd :: args)))
| NCic.Appl args as t ->
(match destroy_nat t with
- | Some n -> idref (Ast.Num (string_of_int n, None))
+ | Some n -> Ast.Num (string_of_int n, None)
| None ->
let args =
if not !hide_coercions then args
args
in
(match args with
- [arg] -> idref (k ~context arg)
- | _ -> idref (Ast.Appl (List.map (k ~context) args))))
+ [arg] -> k ~context arg
+ | _ -> Ast.Appl (List.map (k ~context) args)))
| NCic.Match (NReference.Ref (uri,_) as r,outty,te,patterns) ->
let name = NUri.name_of_uri uri in
-(* CSC
- let uri_str = UriManager.string_of_uri uri in
- let puri_str = sprintf "%s#xpointer(1/%d)" uri_str (typeno+1) in
- let ctor_puri j =
- UriManager.uri_of_string
- (sprintf "%s#xpointer(1/%d/%d)" uri_str (typeno+1) j)
- in
-*)
let case_indty =
- name, None(*CSC Some (UriManager.uri_of_string puri_str)*) in
+ name, Some r in
let constructors, leftno =
let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status r in
let _,_,_,cl = List.nth tys n in
`Pattern -> None
| `Term -> Some case_indty
in
- idref (Ast.Case (k ~context te, indty, Some (k ~context outty), patterns))
+ Ast.Case (k ~context te, indty, Some (k ~context outty), patterns)
;;
-let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term =
+let rec nast_of_cic1 status ~output_type ~metasenv ~subst ~context term =
match Lazy.force status#interp_db.compiled32 term with
| None ->
- nast_of_cic0 status ~idref ~output_type ~metasenv ~subst
- (nast_of_cic1 status ~idref ~output_type ~metasenv ~subst) ~context term
+ nast_of_cic0 status ~output_type ~metasenv ~subst
+ (nast_of_cic1 status ~output_type ~metasenv ~subst) ~context term
| Some (env, ctors, pid) ->
- let idrefs =
- List.map
- (fun term ->
- let attrterm =
- idref
- ~reference:
- (match term with NCic.Const nref -> nref | _ -> assert false)
- (NotationPt.Ident ("dummy",`Ambiguous))
- in
- match attrterm with
- Ast.AttributedTerm (`IdRef id, _) -> id
- | _ -> assert false
- ) ctors
- in
let env =
List.map
(fun (name, term) ->
name,
- nast_of_cic1 status ~idref ~output_type ~subst ~metasenv ~context
+ nast_of_cic1 status ~output_type ~subst ~metasenv ~context
term
) env
in
find_level2_patterns32 status pid
with Not_found -> assert false
in
- let ast = instantiate32 idrefs env symbol args in
- idref ast (*Ast.AttributedTerm (`IdRef (idref term), ast)*)
+ instantiate32 env symbol args
;;
-let nmap_context0 status ~idref ~metasenv ~subst context =
- let module K = Content in
+let nmap_context0 status ~metasenv ~subst context =
let nast_of_cic =
- nast_of_cic1 status ~idref ~output_type:`Term ~metasenv ~subst
+ nast_of_cic1 status ~output_type:`Term ~metasenv ~subst
in
fst (
List.fold_right
(fun item (res,context) ->
match item with
| name,NCic.Decl t ->
- Some
- (* We should call build_decl_item, but we have not computed *)
- (* the inner-types ==> we always produce a declaration *)
- (`Declaration
- { K.dec_name = (Some name);
- K.dec_id = "-1";
- K.dec_inductive = false;
- K.dec_aref = "-1";
- K.dec_type = nast_of_cic ~context t
- })::res,item::context
+ (name, Ast.Decl (nast_of_cic ~context t))::res,
+ item::context
| name,NCic.Def (t,ty) ->
- Some
- (* We should call build_def_item, but we have not computed *)
- (* the inner-types ==> we always produce a declaration *)
- (`Definition
- { K.def_name = (Some name);
- K.def_id = "-1";
- K.def_aref = "-1";
- K.def_term = nast_of_cic ~context t;
- K.def_type = nast_of_cic ~context ty
- })::res,item::context
+ (name, Ast.Def (nast_of_cic ~context t,
+ nast_of_cic ~context ty))::res,
+ item::context
) context ([],[]))
;;
-let nmap_sequent0 status ~idref ~metasenv ~subst (i,(n,context,ty)) =
- let module K = Content in
+let nmap_sequent0 status ~metasenv ~subst (i,(n,context,ty)) =
let nast_of_cic =
- nast_of_cic1 status ~idref ~output_type:`Term ~metasenv ~subst in
- let context' = nmap_context0 status ~idref ~metasenv ~subst context in
- ("-1",i,context',nast_of_cic ~context ty)
+ nast_of_cic1 status ~output_type:`Term ~metasenv ~subst in
+ let context' = nmap_context0 status ~metasenv ~subst context in
+ (i,context',nast_of_cic ~context ty)
;;
let object_prefix = "obj:";;
let inductive_prefix = "ind:";;
let joint_prefix = "joint:";;
+(*
let get_id =
function
Ast.AttributedTerm (`IdRef id, _) -> id
res
;;
-let build_def_item seed context metasenv id n t ty =
- let module K = Content in
-(*
- try
- let sort = Hashtbl.find ids_to_inner_sorts id in
- if sort = `Prop then
- (let p =
- (acic2content seed context metasenv ?name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t)
- in
- `Proof p;)
- else
-*)
- `Definition
- { K.def_name = Some n;
- K.def_id = gen_id definition_prefix seed;
- K.def_aref = id;
- K.def_term = t;
- K.def_type = ty
- }
-(*
- with
- Not_found -> assert false
-*)
-
-let build_decl_item seed id n s =
- let module K = Content in
-(*
- let sort =
- try
- Some (Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id))
- with Not_found -> None
- in
- match sort with
- | Some `Prop ->
- `Hypothesis
- { K.dec_name = name_of n;
- K.dec_id = gen_id declaration_prefix seed;
- K.dec_inductive = false;
- K.dec_aref = id;
- K.dec_type = s
- }
- | _ ->
-*)
- `Declaration
- { K.dec_name = Some n;
- K.dec_id = gen_id declaration_prefix seed;
- K.dec_inductive = false;
- K.dec_aref = id;
- K.dec_type = s
- }
-;;
-
let nmap_obj0 status ~idref (uri,_,metasenv,subst,kind) =
let module K = Content in
let nast_of_cic =
;;
let nmap_obj status = with_idrefs nmap_obj0 status
+*)
+
+let nmap_obj = assert false
-let nmap_sequent status ~metasenv ~subst =
- with_idrefs (nmap_sequent0 ~metasenv ~subst) status
+let nmap_sequent = nmap_sequent0
-let nmap_term status ~metasenv ~subst ~context =
- with_idrefs (nast_of_cic1 ~output_type:`Term ~metasenv ~subst ~context) status
+let nmap_term = nast_of_cic1 ~output_type:`Term
-let nmap_context status ~metasenv ~subst =
- with_idrefs (nmap_context0 ~metasenv ~subst) status
+let nmap_context = nmap_context0
projects / helm.git / commitdiff