* http://helm.cs.unibo.it/
*)
+open Printf
+
type pattern_id = int
+type interpretation_id = pattern_id
type term_info =
{ sort: (Cic.id, CicNotationPt.sort_kind) Hashtbl.t;
let int_set_of_int_list l =
List.fold_left (fun acc i -> IntSet.add i acc) IntSet.empty l
-let (compiled32: (term_info -> Cic.annterm -> CicNotationPt.term) option ref) =
- ref None
-
-let get_compiled32 () =
- match !compiled32 with
- | None -> assert false
- | Some f -> f
-
-let set_compiled32 f = compiled32 := Some f
-
let warning s = prerr_endline ("CicNotation WARNING: " ^ s)
module Patterns =
type row_t = CicNotationPt.cic_appl_pattern list * pattern_id
type t = row_t list
+ let empty = []
+
let first_column t = List.map (fun (patterns, _) -> List.hd patterns) t
let pattern_ids t = List.map snd t
List.split l
end
+ (* acic -> ast auxiliary function s *)
+
let get_types uri =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
let ident_of_name n = Ast.Ident (string_of_name n, None)
+let idref id t = Ast.AttributedTerm (`IdRef id, t)
+
let ast_of_acic0 term_info acic k =
+(* prerr_endline "ast_of_acic0"; *)
let k = k term_info in
let register_uri id uri = Hashtbl.add term_info.uri id uri in
let sort_of_id id =
Hashtbl.find term_info.sort id
with Not_found -> assert false
in
- let idref id t = Ast.AttributedTerm (`IdRef id, t) in
let aux_substs substs =
Some
(List.map
idref id (Ast.LetIn ((ident_of_name n, None), k s, k t))
| Cic.AAppl (aid,args) -> idref aid (Ast.Appl (List.map k args))
| Cic.AConst (id,uri,substs) ->
+ register_uri id (UriManager.string_of_uri uri);
idref id (Ast.Ident (UriManager.name_of_uri uri, aux_substs substs))
- | Cic.AMutInd (id,uri,i,substs) ->
+ | Cic.AMutInd (id,uri,i,substs) as t ->
let name = name_of_inductive_type uri i in
+ let uri_str = UriManager.string_of_uri uri in
+ let puri_str =
+ uri_str ^ "#xpointer(1/" ^ (string_of_int (i + 1)) ^ ")"
+ in
+ register_uri id puri_str;
idref id (Ast.Ident (name, aux_substs substs))
| Cic.AMutConstruct (id,uri,i,j,substs) ->
let name = constructor_of_inductive_type uri i j in
+ let uri_str = UriManager.string_of_uri uri in
+ let puri_str = sprintf "%s#xpointer(1/%d/%d)" uri_str (i + 1) j in
+ register_uri id puri_str;
idref id (Ast.Ident (name, aux_substs substs))
| Cic.AMutCase (id,uri,typeno,ty,te,patterns) ->
let name = name_of_inductive_type uri typeno in
in
aux acic
+ (* persistent state *)
+
+let level2_patterns = Hashtbl.create 211
+
+let (compiled32: (term_info -> Cic.annterm -> CicNotationPt.term) option ref) =
+ ref None
+
+let pattern_matrix = ref Patterns.empty
+
+let get_compiled32 () =
+ match !compiled32 with
+ | None -> assert false
+ | Some f -> f
+
+let set_compiled32 f = compiled32 := Some f
+
(* "envl" is a list of triples:
* <name environment, term environment, pattern id>, where
* name environment: (string * string) list
* term environment: (string * Cic.annterm) list *)
let return_closure success_k =
(fun term_info terms envl ->
+(* prerr_endline "return_closure"; *)
match terms with
| [] ->
(try
let variable_closure names k =
(fun term_info terms envl ->
+(* prerr_endline "variable_closure"; *)
match terms with
| hd :: tl ->
let envl' =
Ast.IdentArg name, _ ->
(name_env, (name, term) :: term_env, pid)
| Ast.EtaArg (Some name, arg'),
- Cic.ALambda (_, name', ty, body) ->
- aux ((name, (string_of_name name', Some ty)) :: name_env)
+ Cic.ALambda (id, name', ty, body) ->
+ aux
+ ((name, (string_of_name name', Some (ty, id))) :: name_env)
term_env pid arg' body
| Ast.EtaArg (Some name, arg'), _ ->
let name' = CicNotationUtil.fresh_name () in
aux ((name, (name', None)) :: name_env)
term_env pid arg' term
- | Ast.EtaArg (None, arg'), Cic.ALambda (_, name, ty, body) ->
+ | Ast.EtaArg (None, arg'), Cic.ALambda (id, name, ty, body) ->
assert false
| Ast.EtaArg (None, arg'), _ ->
assert false
let appl_closure ks k =
(fun term_info terms envl ->
+(* prerr_endline "appl_closure"; *)
(match terms with
| Cic.AAppl (_, args) :: tl ->
(try
let uri_closure ks k =
(fun term_info terms envl ->
+(* prerr_endline "uri_closure"; *)
(match terms with
| [] -> assert false
| hd :: tl ->
+(* prerr_endline (sprintf "uri_of_term = %s" (uri_of_term hd)); *)
begin
try
let k' = List.assoc (uri_of_term hd) ks in
let ast_of_acic1 term_info annterm = (get_compiled32 ()) term_info annterm
-let load_patterns t instantiate =
+let instantiate term_info name_env term_env pid =
+ let symbol, args =
+ try
+ Hashtbl.find level2_patterns pid
+ with Not_found -> assert false
+ in
+ let rec instantiate_arg = function
+ | Ast.IdentArg name ->
+ (try List.assoc name term_env with Not_found -> assert false)
+ | Ast.EtaArg (None, _) -> assert false (* TODO *)
+ | Ast.EtaArg (Some name, arg) ->
+ let (name', ty_opt) =
+ try List.assoc name name_env with Not_found -> assert false
+ in
+ let body = instantiate_arg arg in
+ let name' = Ast.Ident (name', None) in
+ match ty_opt with
+ | None -> Ast.Binder (`Lambda, (name', None), body)
+ | Some (ty, id) ->
+ idref id (Ast.Binder (`Lambda, (name', Some ty), body))
+ in
+ let args' = List.map instantiate_arg args in
+ Ast.Appl (Ast.Symbol (symbol, 0) :: args')
+
+let load_patterns t =
let ast_env_of_name_env term_info name_env =
List.map
(fun (name, (name', ty_opt)) ->
let ast_ty_opt =
match ty_opt with
| None -> None
- | Some annterm -> Some (ast_of_acic1 term_info annterm)
+ | Some (annterm, id) -> Some (ast_of_acic1 term_info annterm, id)
in
(name, (name', ast_ty_opt)))
name_env
let ast = ast_of_acic1 term_info annterm in
ast, term_info.uri
+let fresh_id =
+ let counter = ref ~-1 in
+ fun () ->
+ incr counter;
+ !counter
+
+let add_interpretation (symbol, args) appl_pattern =
+ let id = fresh_id () in
+ Hashtbl.add level2_patterns id (symbol, args);
+ pattern_matrix := ([appl_pattern], id) :: !pattern_matrix;
+ load_patterns !pattern_matrix;
+ id
+
+exception Interpretation_not_found
+
+let remove_interpretation id =
+ (try
+ Hashtbl.remove level2_patterns id;
+ with Not_found -> raise Interpretation_not_found);
+ pattern_matrix := List.filter (fun (_, id') -> id <> id') !pattern_matrix;
+ load_patterns !pattern_matrix
+
+let _ = load_patterns []
+
open Printf
+let _ =
+ Helm_registry.set "getter.mode" "remote";
+ Helm_registry.set "getter.url" "http://helm.cs.unibo.it:58081/"
+
+ (* ORRIBLE HACK! conversion:
+ * (Cic.id, string) Hashtbl.t -> (Cic.id, CicNotationtPt.sort_kind) Hashtbl.t
+ *)
+let patch_sort_tbl tbl =
+ let sort_of_string = function
+ | "Prop" -> `Prop
+ | "Set" -> `Set
+ | "Type" | "?" -> `Type
+ | "CProp" -> `CProp
+ | _ -> assert false
+ in
+ let tbl' = Hashtbl.create (Hashtbl.length tbl) in
+ Hashtbl.iter
+ (fun id sort_str -> Hashtbl.add tbl' id (sort_of_string sort_str))
+ tbl;
+ tbl'
+
let _ =
let module P = CicNotationPt in
let level = ref ~-1 in
| P.Print t ->
print_endline (CicNotationPp.pp_term t); flush stdout
| P.Notation (l1, associativity, precedence, l2) ->
- prerr_endline "foo";
print_endline "Extending notation ..."; flush stdout;
ignore
(CicNotationParser.extend l1 ?precedence ?associativity
(fun env loc ->
prerr_endline "ENV";
prerr_endline (CicNotationPp.pp_env env);
- CicNotationFwd.instantiate_level2 env l2)))
+ CicNotationFwd.instantiate_level2 env l2))
+ | P.Interpretation (l2, l3) ->
+ print_endline "Adding interpretation ..."; flush stdout;
+ let time1 = Unix.gettimeofday () in
+ ignore (CicNotationRew.add_interpretation l2 l3);
+ let time2 = Unix.gettimeofday () in
+ printf "done (patterns compilation took %f seconds)\n"
+ (time2 -. time1);
+ flush stdout
+ | P.Render uri ->
+ let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let annobj, _, _, id_to_sort, _, _, _ =
+ Cic2acic.acic_object_of_cic_object obj
+ in
+ let annterm =
+ match annobj with
+ | Cic.AConstant (_, _, _, _, ty, _, _)
+ | Cic.AVariable (_, _, _, ty, _, _) -> ty
+ | _ -> assert false
+ in
+ let id_to_sort = patch_sort_tbl id_to_sort in
+ let time1 = Unix.gettimeofday () in
+ let t, id_to_uri =
+ CicNotationRew.ast_of_acic id_to_sort annterm
+ in
+ let time2 = Unix.gettimeofday () in
+ printf "ast creation took %f seconds\n" (time2 -. time1);
+ print_endline (CicNotationPp.pp_term t); flush stdout)
(* CicNotationParser.print_l2_pattern ()) *)
| 1 -> ignore (CicNotationParser.parse_syntax_pattern istream)
| 2 ->
projects / helm.git / commitdiff