From: Stefano Zacchiroli Date: Tue, 31 May 2005 15:41:21 +0000 (+0000) Subject: snapshot (first version with [apparently] working mappings between level X-Git-Tag: PRE_INDEX_1~87 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7f72a2bf9a6f79c58048c594dc390265365face8;p=helm.git snapshot (first version with [apparently] working mappings between level 2 and level 3) --- diff --git a/helm/ocaml/cic_notation/Makefile b/helm/ocaml/cic_notation/Makefile index b38315464..a976a283d 100644 --- a/helm/ocaml/cic_notation/Makefile +++ b/helm/ocaml/cic_notation/Makefile @@ -28,6 +28,7 @@ LOCAL_LINKOPTS = -package helm-cic_notation -linkpkg test: test_lexer test_parser test_lexer: test_lexer.ml $(PACKAGE).cma $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< +test_parser: REQUIRES += helm-cic_omdoc test_parser: test_parser.ml $(PACKAGE).cma $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index d282e3d70..b408e6e3b 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -565,25 +565,27 @@ EXTEND [ IDENT "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ] ]; notation: [ - [ IDENT "notation"; - p1 = level1_pattern; + [ p1 = level1_pattern; assoc = OPT associativity; prec = OPT precedence; IDENT "for"; p2 = level2_pattern -> (p1, assoc, prec, p2) ] ]; interpretation: [ - [ IDENT "interpretation"; s = SYMBOL; args = LIST1 argument; IDENT "as"; + [ s = SYMBOL; args = LIST1 argument; SYMBOL "="; t = level3_term -> - () + (s, args, t) ] ]; (* }}} *) (* {{{ Top-level phrases *) phrase: [ [ IDENT "print"; p2 = level2_pattern; SYMBOL "." -> Print p2 - | (l1, assoc, prec, l2) = notation; SYMBOL "." -> + | IDENT "notation"; (l1, assoc, prec, l2) = notation; SYMBOL "." -> Notation (l1, assoc, prec, l2) + | IDENT "interpretation"; (symbol, args, l3) = interpretation; SYMBOL "." -> + Interpretation ((symbol, args), l3) + | IDENT "render"; u = URI; SYMBOL "." -> Render (UriManager.uri_of_string u) ] ]; (* }}} *) diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml index e9683521e..b8fdcfac6 100644 --- a/helm/ocaml/cic_notation/cicNotationPt.ml +++ b/helm/ocaml/cic_notation/cicNotationPt.ml @@ -141,4 +141,6 @@ type phrase = (* TODO hackish: replace with TacticAst.statement or similar *) | Print of term | Notation of term * Gramext.g_assoc option * int option * term (* level 1 pattern, associativity, precedence, level 2 pattern *) + | Interpretation of (string * argument_pattern list) * cic_appl_pattern + | Render of UriManager.uri diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index 8253efd16..a3a06f922 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -23,7 +23,10 @@ * 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; @@ -43,16 +46,6 @@ module IntSet = Set.Make (OrderedInt) 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 = @@ -60,6 +53,8 @@ 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 @@ -130,6 +125,8 @@ module Patterns = 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 @@ -163,7 +160,10 @@ let string_of_name = function 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 = @@ -171,7 +171,6 @@ let ast_of_acic0 term_info acic k = 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 @@ -211,12 +210,21 @@ let ast_of_acic0 term_info acic k = 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 @@ -268,12 +276,29 @@ let ast_of_acic0 term_info acic k = 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: * , 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 @@ -283,6 +308,7 @@ let return_closure success_k = let variable_closure names k = (fun term_info terms envl -> +(* prerr_endline "variable_closure"; *) match terms with | hd :: tl -> let envl' = @@ -293,14 +319,15 @@ let variable_closure names k = 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 @@ -313,6 +340,7 @@ let variable_closure names k = let appl_closure ks k = (fun term_info terms envl -> +(* prerr_endline "appl_closure"; *) (match terms with | Cic.AAppl (_, args) :: tl -> (try @@ -326,9 +354,11 @@ let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t) 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 @@ -439,14 +469,38 @@ let compiler32 (t: Patterns.t) success_k fail_k = 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 @@ -470,3 +524,27 @@ let ast_of_acic id_to_sort annterm = 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 [] + diff --git a/helm/ocaml/cic_notation/cicNotationRew.mli b/helm/ocaml/cic_notation/cicNotationRew.mli index cac67cb21..fbd0ea166 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.mli +++ b/helm/ocaml/cic_notation/cicNotationRew.mli @@ -29,3 +29,15 @@ val ast_of_acic: CicNotationPt.term (* ast *) * (Cic.id, string) Hashtbl.t (* id -> uri *) +type interpretation_id + +val add_interpretation: + string * CicNotationPt.argument_pattern list -> (* level 2 pattern *) + CicNotationPt.cic_appl_pattern -> (* level 3 pattern *) + interpretation_id + +exception Interpretation_not_found + + (** @raise Interpretation_not_found *) +val remove_interpretation: interpretation_id -> unit + diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index 6e0160e7a..05a80d982 100644 --- a/helm/ocaml/cic_notation/test_parser.ml +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -25,6 +25,27 @@ 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 @@ -78,14 +99,40 @@ let _ = | 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 ->