open Printf
-module Ast = CicNotationPt
+module Ast = NotationPt
let debug = false
let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
type id = string
-(*
-type interpretation_id = int
-
-type term_info =
- { sort: (Cic.id, Ast.sort_kind) Hashtbl.t;
- uri: (Cic.id, UriManager.uri) Hashtbl.t;
- }
+let hide_coercions = ref true;;
-let get_types uri =
- let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
- match o with
- | Cic.InductiveDefinition (l,_,leftno,_) -> l, leftno
- | _ -> assert false
-*)
+class status =
+ object
+ inherit NCicCoercion.status
+ inherit Interpretations.status
+ end
let idref register_ref =
let id = ref 0 in
(* CODICE c&p da NCicPp *)
let nast_of_cic0 status
~(idref:
- ?reference:NReference.reference -> CicNotationPt.term -> CicNotationPt.term)
+ ?reference:NReference.reference -> NotationPt.term -> NotationPt.term)
~output_type ~metasenv ~subst k ~context =
function
| NCic.Rel n ->
| Some n -> idref (Ast.Num (string_of_int n, -1))
| None ->
let args =
- if not !Acic2content.hide_coercions then args
+ if not !hide_coercions then args
else
match
NCicCoercion.match_coercion status ~metasenv ~context ~subst t
idref (Ast.Case (k ~context te, indty, Some (k ~context outty), patterns))
;;
- (* persistent state *)
-
-(*
-let initial_level2_patterns32 () = Hashtbl.create 211
-let initial_interpretations () = Hashtbl.create 211
-
-let level2_patterns32 = ref (initial_level2_patterns32 ())
-(* symb -> id list ref *)
-let interpretations = ref (initial_interpretations ())
-*)
let compiled32 = ref None
-(*
-let pattern32_matrix = ref []
-let counter = ref ~-1
-
-let stack = ref []
-
-let push () =
- stack := (!counter,!level2_patterns32,!interpretations,!compiled32,!pattern32_matrix)::!stack;
- counter := ~-1;
- level2_patterns32 := initial_level2_patterns32 ();
- interpretations := initial_interpretations ();
- compiled32 := None;
- pattern32_matrix := []
-;;
-
-let pop () =
- match !stack with
- [] -> assert false
- | (ocounter,olevel2_patterns32,ointerpretations,ocompiled32,opattern32_matrix)::old ->
- stack := old;
- counter := ocounter;
- level2_patterns32 := olevel2_patterns32;
- interpretations := ointerpretations;
- compiled32 := ocompiled32;
- pattern32_matrix := opattern32_matrix
-;;
-*)
let get_compiled32 () =
match !compiled32 with
in
let rec add_lambda t n =
if n > 0 then
- let name = CicNotationUtil.fresh_name () in
+ let name = NotationUtil.fresh_name () in
Ast.Binder (`Lambda, (Ast.Ident (name, None), None),
Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, None)])
else
idref
~reference:
(match term with NCic.Const nref -> nref | _ -> assert false)
- (CicNotationPt.Ident ("dummy",None))
+ (NotationPt.Ident ("dummy",None))
in
match attrterm with
Ast.AttributedTerm (`IdRef id, _) -> id
in
let _, symbol, args, _ =
try
- TermAcicContent.find_level2_patterns32 pid
+ Interpretations.find_level2_patterns32 status pid
with Not_found -> assert false
in
let ast = instantiate32 idrefs env symbol args in
HExtlib.filter_map (function (true, ap, id) -> Some (ap, id) | _ -> None) t
in
set_compiled32 (lazy (Ncic2astMatcher.Matcher32.compiler t))
-in
- TermAcicContent.add_load_patterns32 load_patterns32;
- TermAcicContent.init ()
;;
-(*
-let ast_of_acic ~output_type id_to_sort annterm =
- debug_print (lazy ("ast_of_acic <- "
- ^ CicPp.ppterm (Deannotate.deannotate_term annterm)));
- let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in
- let ast = ast_of_acic1 ~output_type term_info annterm in
- debug_print (lazy ("ast_of_acic -> " ^ CicNotationPp.pp_term ast));
- ast, term_info.uri
-
-let fresh_id =
- fun () ->
- incr counter;
- !counter
-
-let add_interpretation dsc (symbol, args) appl_pattern =
- let id = fresh_id () in
- Hashtbl.add !level2_patterns32 id (dsc, symbol, args, appl_pattern);
- pattern32_matrix := (true, appl_pattern, id) :: !pattern32_matrix;
- load_patterns32 !pattern32_matrix;
- (try
- let ids = Hashtbl.find !interpretations symbol in
- ids := id :: !ids
- with Not_found -> Hashtbl.add !interpretations symbol (ref [id]));
- id
-
-let get_all_interpretations () =
- List.map
- (function (_, _, id) ->
- let (dsc, _, _, _) =
- try
- Hashtbl.find !level2_patterns32 id
- with Not_found -> assert false
- in
- (id, dsc))
- !pattern32_matrix
-
-let get_active_interpretations () =
- HExtlib.filter_map (function (true, _, id) -> Some id | _ -> None)
- !pattern32_matrix
-
-let set_active_interpretations ids =
- let pattern32_matrix' =
- List.map
- (function
- | (_, ap, id) when List.mem id ids -> (true, ap, id)
- | (_, ap, id) -> (false, ap, id))
- !pattern32_matrix
- in
- pattern32_matrix := pattern32_matrix';
- load_patterns32 !pattern32_matrix
-
-exception Interpretation_not_found
-
-let lookup_interpretations symbol =
- try
- HExtlib.list_uniq
- (List.sort Pervasives.compare
- (List.map
- (fun id ->
- let (dsc, _, args, appl_pattern) =
- try
- Hashtbl.find !level2_patterns32 id
- with Not_found -> assert false
- in
- dsc, args, appl_pattern)
- !(Hashtbl.find !interpretations symbol)))
- with Not_found -> raise Interpretation_not_found
-
-let remove_interpretation id =
- (try
- let dsc, symbol, _, _ = Hashtbl.find !level2_patterns32 id in
- let ids = Hashtbl.find !interpretations symbol in
- ids := List.filter ((<>) id) !ids;
- Hashtbl.remove !level2_patterns32 id;
- with Not_found -> raise Interpretation_not_found);
- pattern32_matrix :=
- List.filter (fun (_, _, id') -> id <> id') !pattern32_matrix;
- load_patterns32 !pattern32_matrix
-
-let _ = load_patterns32 []
-
-let instantiate_appl_pattern
- ~mk_appl ~mk_implicit ~term_of_uri env appl_pattern
-=
- let lookup name =
- try List.assoc name env
- with Not_found ->
- prerr_endline (sprintf "Name %s not found" name);
- assert false
- in
- let rec aux = function
- | Ast.UriPattern uri -> term_of_uri uri
- | Ast.ImplicitPattern -> mk_implicit false
- | Ast.VarPattern name -> lookup name
- | Ast.ApplPattern terms -> mk_appl (List.map aux terms)
- in
- aux appl_pattern
-*)
-
let nmap_sequent0 status ~idref ~metasenv ~subst (i,(n,context,ty)) =
let module K = Content in
let nast_of_cic =
let res =
match kind with
| NCic.Fixpoint (is_rec, ifl, _) ->
- (gen_id object_prefix seed, [], conjectures,
+ (gen_id object_prefix seed, conjectures,
`Joint
{ K.joint_id = gen_id joint_prefix seed;
K.joint_kind =
K.joint_defs = List.map (build_fixpoint is_rec seed) ifl
})
| NCic.Inductive (is_ind, lno, itl, _) ->
- (gen_id object_prefix seed, [], conjectures,
+ (gen_id object_prefix seed, conjectures,
`Joint
{ K.joint_id = gen_id joint_prefix seed;
K.joint_kind =
| NCic.Constant (_,_,Some bo,ty,_) ->
let ty = nast_of_cic ~context:[] ty in
let bo = nast_of_cic ~context:[] bo in
- (gen_id object_prefix seed, [], conjectures,
+ (gen_id object_prefix seed, conjectures,
`Def (K.Const,ty,
build_def_item seed [] [] (get_id bo) (NUri.name_of_uri uri) bo ty))
| NCic.Constant (_,_,None,ty,_) ->
let ty = nast_of_cic ~context:[] ty in
- (gen_id object_prefix seed, [], conjectures,
+ (gen_id object_prefix seed, conjectures,
`Decl (K.Const,
(*CSC: ??? get_id ty here used to be the id of the axiom! *)
build_decl_item seed (get_id ty) (NUri.name_of_uri uri) ty))
in
res,ids_to_refs
;;
+
+Interpretations.set_load_patterns32 load_patterns32
projects / helm.git / blobdiff