X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationRew.ml;h=15947f3f238b00d0f9ad875c221f04e3a2e0127a;hb=34113d572c334c351ba66f4b05db503eed4d48f2;hp=8253efd161735b99f459062fe67afd8ba4af658a;hpb=724827ba7e5c1419229382487bed53f7dbb862db;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index 8253efd16..15947f3f2 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -23,113 +23,20 @@ * http://helm.cs.unibo.it/ *) +open Printf + type pattern_id = int +type interpretation_id = pattern_id +type pretty_printer_id = pattern_id + +let default_prec = 50 +let default_assoc = Gramext.NonA type term_info = { sort: (Cic.id, CicNotationPt.sort_kind) Hashtbl.t; uri: (Cic.id, string) Hashtbl.t; } -exception No_match - -module OrderedInt = - struct - type t = int - let compare (x1:t) (x2:t) = Pervasives.compare x2 x1 (* reverse order *) - end - -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 = - struct - type row_t = CicNotationPt.cic_appl_pattern list * pattern_id - type t = row_t list - - let first_column t = List.map (fun (patterns, _) -> List.hd patterns) t - let pattern_ids t = List.map snd t - - let prepend_column t column = - try - List.map2 (fun elt (pl, pid) -> (elt :: pl), pid) column t - - with Invalid_argument _ -> assert false - - let prepend_columns t columns = - List.fold_right - (fun column rows -> prepend_column rows column) - columns t - - let partition t pidl = - let partitions = Hashtbl.create 11 in - let add pid row = Hashtbl.add partitions pid row in - (try - List.iter2 add pidl t - with Invalid_argument _ -> assert false); - let pidset = int_set_of_int_list pidl in - IntSet.fold - (fun pid acc -> - match Hashtbl.find_all partitions pid with - | [] -> acc - | patterns -> (pid, List.rev patterns) :: acc) - pidset [] - - let are_empty t = fst (List.hd t) = [] - (* if first row has an empty list of patterns, then others will as well *) - - (* return 2 lists of rows, first one containing homogeneous rows according - * to "compatible" below *) - let horizontal_split t = - let compatible ap1 ap2 = - match ap1, ap2 with - | CicNotationPt.UriPattern _, CicNotationPt.UriPattern _ - | CicNotationPt.ArgPattern _, CicNotationPt.ArgPattern _ - | CicNotationPt.ApplPattern _, CicNotationPt.ApplPattern _ -> true - | _ -> false - in - let ap = - match t with - | [] -> assert false - | ([], _) :: _ -> - assert false (* are_empty should have been invoked in advance *) - | (hd :: _ , _) :: _ -> hd - in - let rec aux prev_t = function - | [] -> List.rev prev_t, [] - | ([], _) :: _ -> assert false - | (((hd :: _), _) as row) :: tl when compatible ap hd -> - aux (row :: prev_t) tl - | t -> List.rev prev_t, t - in - aux [] t - - (* return 2 lists, first one representing first column, second one - * representing rows stripped of the first element *) - let vertical_split t = - let l = - List.map - (function - | (hd :: tl, pid) -> hd, (tl, pid) - | _ -> assert false) - t - in - List.split l - end - let get_types uri = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with @@ -156,6 +63,7 @@ let constructor_of_inductive_type uri i j = with Not_found -> assert false) module Ast = CicNotationPt +module Parser = CicNotationParser let string_of_name = function | Cic.Name s -> s @@ -163,6 +71,61 @@ 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 resolve_binder = function + | `Lambda -> "\\lambda" + | `Pi -> "\\Pi" + | `Forall -> "\\forall" + | `Exists -> "\\exists" + +let binder_attributes = [None, "mathcolor", "blue"] +let atop_attributes = [None, "linethickness", "0pt"] +let indent_attributes = [None, "indent", "1em"] +let keyword_attributes = [None, "mathcolor", "blue"] + +let pp_ast0 t k = + let reset_href t = Ast.AttributedTerm (`Href [], t) in + let builtin_symbol s = reset_href (Ast.Literal (`Symbol s)) in + let binder_symbol s = + Ast.AttributedTerm (`XmlAttrs binder_attributes, builtin_symbol s) + in + let rec aux = function + | Ast.Appl ts -> + Ast.AttributedTerm (`Level (Parser.apply_prec, Parser.apply_assoc), + Ast.Layout + (Ast.Box ((Ast.HOV, true, true), + (CicNotationUtil.dress + (Ast.Layout Ast.Break) + (List.map k ts))))) + | Ast.Binder (`Forall, (Ast.Ident ("_", _), ty), body) + | Ast.Binder (`Pi, (Ast.Ident ("_", _), ty), body) -> + Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc), + Ast.Layout (Ast.Box ((Ast.HV, false, true), [ + aux_ty ty; + Ast.Layout Ast.Break; + binder_symbol "\\to"; + k body]))) + | Ast.Binder (binder_kind, (id, ty), body) -> + Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc), + Ast.Layout (Ast.Box ((Ast.HV, false, true), [ + binder_symbol (resolve_binder binder_kind); + k id; + builtin_symbol ":"; + aux_ty ty; + Ast.Layout Ast.Break; + builtin_symbol "."; + k body ]))) + | t -> CicNotationUtil.visit_ast ~special_k k t + and aux_ty = function + | None -> builtin_symbol "?" + | Some ty -> k ty + and special_k = function + | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, k t) + | _ -> assert false + in + aux t + let ast_of_acic0 term_info acic k = let k = k term_info in let register_uri id uri = Hashtbl.add term_info.uri id uri in @@ -171,7 +134,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 +173,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,205 +239,225 @@ let ast_of_acic0 term_info acic k = in aux acic - (* "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 -> - match terms with - | [] -> - (try - success_k term_info (List.hd envl) - with Failure _ -> assert false) - | _ -> assert false) - -let variable_closure names k = - (fun term_info terms envl -> - match terms with - | hd :: tl -> - let envl' = - List.map2 - (fun arg (name_env, term_env, pid) -> - let rec aux name_env term_env pid arg term = - match arg, term with - 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) - 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) -> - assert false - | Ast.EtaArg (None, arg'), _ -> - assert false - in - aux name_env term_env pid arg hd) - names envl - in - k term_info tl envl' - | _ -> assert false) - -let appl_closure ks k = - (fun term_info terms envl -> - (match terms with - | Cic.AAppl (_, args) :: tl -> - (try - let k' = List.assoc (List.length args) ks in - k' term_info (args @ tl) envl - with Not_found -> k term_info terms envl) - | [] -> assert false - | _ -> k term_info terms envl)) - -let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t) - -let uri_closure ks k = - (fun term_info terms envl -> - (match terms with - | [] -> assert false - | hd :: tl -> - begin - try - let k' = List.assoc (uri_of_term hd) ks in - k' term_info tl envl - with - | Invalid_argument _ (* raised by uri_of_term *) - | Not_found -> k term_info terms envl - end)) - - (* compiler from level 3 to level 2 *) -let compiler32 (t: Patterns.t) success_k fail_k = - let rec aux t k = (* k is a continuation *) - if t = [] then - k - else if Patterns.are_empty t then begin - (match t with - | _::_::_ -> warning "Ambiguous patterns" - | _ -> ()); - return_closure success_k - end else - match Patterns.horizontal_split t with - | t', [] -> - (match t' with - | [] - | ([], _) :: _ -> assert false - | (Ast.ArgPattern (Ast.IdentArg _) :: _, _) :: _ - | (Ast.ArgPattern (Ast.EtaArg _) :: _, _) :: _ -> - let first_column, t'' = Patterns.vertical_split t' in - let names = - List.map - (function - | Ast.ArgPattern arg -> arg - | _ -> assert false) - first_column - in - variable_closure names (aux t'' k) - | (Ast.ApplPattern _ :: _, _) :: _ -> - let pidl = - List.map - (function - | (Ast.ApplPattern args) :: _, _ -> List.length args - | _ -> assert false) - t' - in - (* arity partitioning *) - let clusters = Patterns.partition t' pidl in - let ks = (* k continuation list *) - List.map - (fun (len, cluster) -> - let cluster' = - List.map (* add args as patterns heads *) - (function - | (Ast.ApplPattern args) :: tl, pid -> - (* let's throw away "teste di cluster" *) - args @ tl, pid - | _ -> assert false) - cluster - in - len, aux cluster' k) - clusters - in - appl_closure ks k - | (Ast.UriPattern _ :: _, _) :: _ -> - let uidmap, pidl = - let urimap = ref [] in - let uidmap = ref [] in - let get_uri_id uri = - try - List.assoc uri !urimap - with - Not_found -> - let uid = List.length !urimap in - urimap := (uri, uid) :: !urimap ; - uidmap := (uid, uri) :: !uidmap ; - uid - in - let uidl = - List.map - (function - | (Ast.UriPattern uri) :: _, _ -> get_uri_id uri - | _ -> assert false) - t' - in - !uidmap, uidl - in - let clusters = Patterns.partition t' pidl in - let ks = - List.map - (fun (uid, cluster) -> - let cluster' = - List.map - (function - | (Ast.UriPattern uri) :: tl, pid -> tl, pid - | _ -> assert false) - cluster - in - List.assoc uid uidmap, aux cluster' k) - clusters - in - uri_closure ks k) - | t', tl -> aux t' (aux tl k) - in - let matcher = aux t (fun _ _ -> raise No_match) in - (fun term_info annterm -> - try - matcher term_info [annterm] (List.map (fun (_, pid) -> [], [], pid) t) - with No_match -> fail_k term_info annterm) + (* persistent state *) -let ast_of_acic1 term_info annterm = (get_compiled32 ()) term_info annterm +let level1_patterns21 = Hashtbl.create 211 +let level2_patterns32 = Hashtbl.create 211 -let load_patterns t instantiate = - 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) +let compiled21 = ref None +let compiled32 = ref None + +let pattern21_matrix = ref [] +let pattern32_matrix = ref [] + +let get_compiled21 () = + match !compiled21 with + | None -> assert false + | Some f -> Lazy.force f +let get_compiled32 () = + match !compiled32 with + | None -> assert false + | Some f -> Lazy.force f + +let set_compiled21 f = compiled21 := Some f +let set_compiled32 f = compiled32 := Some f + +let instantiate21 env (* precedence associativity *) l1 = + let rec subst_singleton env t = + CicNotationUtil.group (subst env t) + and subst env = function + | Ast.AttributedTerm (_, t) -> subst env t + | Ast.Variable var -> + let name, expected_ty = CicNotationEnv.declaration_of_var var in + let ty, value = + try + List.assoc name env + with Not_found -> assert false in - (name, (name', ast_ty_opt))) - name_env + assert (CicNotationEnv.well_typed ty value); (* INVARIANT *) + (* following assertion should be a conditional that makes this + * instantiation fail *) + assert (CicNotationEnv.well_typed expected_ty value); + [ CicNotationEnv.term_of_value value ] + | Ast.Magic m -> subst_magic env m + | Ast.Literal (`Keyword k) as t -> + [ Ast.AttributedTerm (`XmlAttrs keyword_attributes, t) ] + | Ast.Literal _ as t -> [ t ] + | Ast.Layout l -> [ Ast.Layout (subst_layout env l) ] + | t -> [ CicNotationUtil.visit_ast (subst_singleton env) t ] + and subst_magic env = function + | Ast.List0 (p, sep_opt) + | Ast.List1 (p, sep_opt) -> + let rec_decls = CicNotationEnv.declarations_of_term p in + let rec_values = + List.map (fun (n, _) -> CicNotationEnv.lookup_list env n) rec_decls + in + let values = CicNotationUtil.ncombine rec_values in + let sep = + match sep_opt with + | None -> [] + | Some l -> [ CicNotationPt.Literal l ] + in + let rec instantiate_list acc = function + | [] -> List.rev acc + | value_set :: [] -> + let env = CicNotationEnv.combine rec_decls value_set in + instantiate_list (CicNotationUtil.group (subst env p) :: acc) [] + | value_set :: tl -> + let env = CicNotationEnv.combine rec_decls value_set in + instantiate_list (CicNotationUtil.group ((subst env p) @ sep) :: acc) tl + in + instantiate_list [] values + | Ast.Opt p -> + let opt_decls = CicNotationEnv.declarations_of_term p in + let env = + let rec build_env = function + | [] -> [] + | (name, ty) :: tl -> + (* assumption: if one of the value is None then all are *) + (match CicNotationEnv.lookup_opt env name with + | None -> raise Exit + | Some v -> (name, (ty, v)) :: build_env tl) + in + try build_env opt_decls with Exit -> [] + in + begin + match env with + | [] -> [] + | _ -> subst env p + end + | _ -> assert false (* impossible *) + and subst_layout env = function + | Ast.Box (kind, tl) -> + Ast.Box (kind, List.concat (List.map (subst env) tl)) + | l -> CicNotationUtil.visit_layout (subst_singleton env) l in - let ast_env_of_term_env term_info = - List.map (fun (name, term) -> (name, ast_of_acic1 term_info term)) + subst_singleton env l1 + +let rec pp_ast1 term = + let rec pp_value = function + | CicNotationEnv.NumValue _ as v -> v + | CicNotationEnv.StringValue _ as v -> v +(* | CicNotationEnv.TermValue t when t == term -> CicNotationEnv.TermValue (pp_ast0 t pp_ast1) *) + | CicNotationEnv.TermValue t -> CicNotationEnv.TermValue (pp_ast1 t) + | CicNotationEnv.OptValue None as v -> v + | CicNotationEnv.OptValue (Some v) -> + CicNotationEnv.OptValue (Some (pp_value v)) + | CicNotationEnv.ListValue vl -> + CicNotationEnv.ListValue (List.map pp_value vl) in - let fail_k term_info annterm = ast_of_acic0 term_info annterm ast_of_acic1 in - let success_k term_info (name_env, term_env, pid) = - instantiate - term_info - (ast_env_of_name_env term_info name_env) - (ast_env_of_term_env term_info term_env) - pid + let ast_env_of_env env = + List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env in - let compiled32 = compiler32 t success_k fail_k in - set_compiled32 compiled32 + match term with + | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, pp_ast1 t) + | _ -> + begin + match (get_compiled21 ()) term with + | None -> pp_ast0 term pp_ast1 + | Some (env, pid) -> + let precedence, associativity, l1 = + try + Hashtbl.find level1_patterns21 pid + with Not_found -> assert false + in + Ast.AttributedTerm (`Level (precedence, associativity), + (instantiate21 (ast_env_of_env env) l1)) + end + +let instantiate32 term_info env symbol args = + let rec instantiate_arg = function + | GrafiteAst.IdentArg (n, name) -> + let t = (try List.assoc name env with Not_found -> assert false) in + let rec count_lambda = function + | Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body + | _ -> 0 + in + let rec add_lambda t n = + if n > 0 then + let name = CicNotationUtil.fresh_name () in + Ast.Binder (`Lambda, (Ast.Ident (name, None), None), + Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, None)]) + else + t + in + add_lambda t (n - count_lambda t) + in + let args' = List.map instantiate_arg args in + Ast.Appl (Ast.Symbol (symbol, 0) :: args') + +let rec ast_of_acic1 term_info annterm = + match (get_compiled32 ()) annterm with + | None -> ast_of_acic0 term_info annterm ast_of_acic1 + | Some (env, pid) -> + let env' = + List.map (fun (name, term) -> (name, ast_of_acic1 term_info term)) env + in + let symbol, args, uris = + try + Hashtbl.find level2_patterns32 pid + with Not_found -> assert false + in + let ast = instantiate32 term_info env' symbol args in + match uris with + | [] -> ast + | _ -> Ast.AttributedTerm (`Href uris, ast) + +let load_patterns32 t = + set_compiled32 (lazy (CicNotationMatcher.Matcher32.compiler t)) + +let load_patterns21 t = + set_compiled21 (lazy (CicNotationMatcher.Matcher21.compiler t)) let ast_of_acic id_to_sort annterm = let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in let ast = ast_of_acic1 term_info annterm in ast, term_info.uri +let pp_ast term = pp_ast1 term + +let fresh_id = + let counter = ref ~-1 in + fun () -> + incr counter; + !counter + +let add_interpretation (symbol, args) appl_pattern = + let id = fresh_id () in + let uris = CicNotationUtil.find_appl_pattern_uris appl_pattern in + Hashtbl.add level2_patterns32 id (symbol, args, uris); + pattern32_matrix := (appl_pattern, id) :: !pattern32_matrix; + load_patterns32 !pattern32_matrix; + id + +let add_pretty_printer + ?(precedence = default_prec) ?(associativity = default_assoc) l2 l1 += + let id = fresh_id () in + let l2' = CicNotationUtil.strip_attributes l2 in + Hashtbl.add level1_patterns21 id (precedence, associativity, l1); + pattern21_matrix := (l2', id) :: !pattern21_matrix; + load_patterns21 !pattern21_matrix; + id + +exception Interpretation_not_found +exception Pretty_printer_not_found + +let remove_interpretation id = + (try + 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 remove_pretty_printer id = + (try + Hashtbl.remove level1_patterns21 id; + with Not_found -> raise Pretty_printer_not_found); + pattern21_matrix := List.filter (fun (_, id') -> id <> id') !pattern21_matrix; + load_patterns21 !pattern21_matrix + +let _ = + load_patterns21 []; + load_patterns32 [] +