X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationRew.ml;h=8bbc22e24344819e37e7758abe8c5dc6f54f8f40;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=73f66771f8869695e9c90958b78a73ae88bcab79;hpb=98d5d40127827a5c40e58cb0c9654066f940b0ea;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index 73f66771f..8bbc22e24 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -28,7 +28,7 @@ open Printf module Ast = CicNotationPt let debug = false -let debug_print = if debug then prerr_endline else ignore +let debug_print s = if debug then prerr_endline (Lazy.force s) else () type pattern_id = int type interpretation_id = pattern_id @@ -36,7 +36,7 @@ type pretty_printer_id = pattern_id type term_info = { sort: (Cic.id, Ast.sort_kind) Hashtbl.t; - uri: (Cic.id, string) Hashtbl.t; + uri: (Cic.id, UriManager.uri) Hashtbl.t; } let get_types uri = @@ -73,6 +73,17 @@ let resolve_binder = function | `Exists -> "\\exists" let add_level_info prec assoc t = Ast.AttributedTerm (`Level (prec, assoc), t) +let add_pos_info pos t = Ast.AttributedTerm (`ChildPos pos, t) +let left_pos = add_pos_info `Left +let right_pos = add_pos_info `Right +let inner_pos = add_pos_info `Inner + +let rec top_pos t = add_level_info ~-1 Gramext.NonA (inner_pos t) +(* function + | Ast.AttributedTerm (`Level _, t) -> + add_level_info ~-1 Gramext.NonA (inner_pos t) + | Ast.AttributedTerm (attr, t) -> Ast.AttributedTerm (attr, top_pos t) + | t -> add_level_info ~-1 Gramext.NonA (inner_pos t) *) let rec remove_level_info = function @@ -80,7 +91,8 @@ let rec remove_level_info = | Ast.AttributedTerm (a, t) -> Ast.AttributedTerm (a, remove_level_info t) | t -> t -let add_xml_attrs attrs t = Ast.AttributedTerm (`XmlAttrs attrs, t) +let add_xml_attrs attrs t = + if attrs = [] then t else Ast.AttributedTerm (`XmlAttrs attrs, t) let add_keyword_attrs = add_xml_attrs (RenderingAttrs.keyword_attributes `MathML) @@ -93,15 +105,12 @@ let vbox = box Ast.V let hvbox = box Ast.HV let hovbox = box Ast.HOV let break = Ast.Layout Ast.Break -(* let reset_href t = Ast.AttributedTerm (`Href [], t) *) -let reset_href t = t -let builtin_symbol s = reset_href (Ast.Literal (`Symbol s)) -let keyword k = reset_href (add_keyword_attrs (Ast.Literal (`Keyword k))) +let builtin_symbol s = Ast.Literal (`Symbol s) +let keyword k = add_keyword_attrs (Ast.Literal (`Keyword k)) let number s = - reset_href - (add_xml_attrs (RenderingAttrs.number_attributes `MathML) - (Ast.Literal (`Number s))) + add_xml_attrs (RenderingAttrs.number_attributes `MathML) + (Ast.Literal (`Number s)) let ident i = add_xml_attrs (RenderingAttrs.ident_attributes `MathML) (Ast.Ident (i, None)) @@ -109,7 +118,9 @@ let ident i = let ident_w_href href i = match href with | None -> ident i - | Some href -> Ast.AttributedTerm (`Href [href], ident i) + | Some href -> + let href = UriManager.string_of_uri href in + add_xml_attrs [Some "xlink", "href", href] (ident i) let binder_symbol s = add_xml_attrs (RenderingAttrs.builtin_symbol_attributes `MathML) @@ -119,37 +130,53 @@ let string_of_sort_kind = function | `Prop -> "Prop" | `Set -> "Set" | `CProp -> "CProp" - | `Type -> "Type" + | `Type _ -> "Type" let pp_ast0 t k = - let rec aux = function + let rec aux = + function | Ast.Appl ts -> + let rec aux_args pos = + function + | [] -> [] + | [ last ] -> + let last = k last in + if pos = `Left then [ left_pos last ] else [ right_pos last ] + | hd :: tl -> + (add_pos_info pos (k hd)) :: aux_args `Inner tl + in add_level_info Ast.apply_prec Ast.apply_assoc - (hovbox true true (CicNotationUtil.dress break (List.map k ts))) + (hovbox true true (CicNotationUtil.dress break (aux_args `Left ts))) | Ast.Binder (binder_kind, (id, ty), body) -> add_level_info Ast.binder_prec Ast.binder_assoc (hvbox false true [ binder_symbol (resolve_binder binder_kind); k id; builtin_symbol ":"; aux_ty ty; break; - builtin_symbol "."; k body ]) + builtin_symbol "."; right_pos (k body) ]) | Ast.Case (what, indty_opt, outty_opt, patterns) -> let outty_box = match outty_opt with | None -> [] | Some outty -> - [ builtin_symbol "["; remove_level_info (k outty); - builtin_symbol "]"; break ] + [ keyword "return"; break; remove_level_info (k outty)] in let indty_box = match indty_opt with | None -> [] - | Some (indty, href) -> [ keyword "in"; ident_w_href href indty ] + | Some (indty, href) -> [ keyword "in"; break; ident_w_href href indty ] in let match_box = - hvbox false true [ - keyword "match"; break; - hvbox false false ([ k what ] @ indty_box); break; - keyword "with" ] + hvbox false false [ + hvbox false true [ + hvbox false true [ keyword "match"; break; top_pos (k what) ]; + break; + hvbox false true indty_box; + break; + hvbox false true outty_box + ]; + break; + keyword "with" + ] in let mk_case_pattern (head, href, vars) = hbox true false (ident_w_href href head :: List.map aux_var vars) @@ -161,7 +188,7 @@ let pp_ast0 t k = (hvbox false true [ hbox false true [ mk_case_pattern lhs; builtin_symbol "\\Rightarrow" ]; - break; k rhs ])) + break; top_pos (k rhs) ])) patterns in let patterns'' = @@ -188,20 +215,20 @@ let pp_ast0 t k = in add_level_info Ast.simple_prec Ast.simple_assoc (hvbox false false [ - hvbox false false (outty_box @ [ match_box ]); break; + hvbox false false ([match_box]); break; hbox false false [ hvbox false false patterns'' ] ]) | Ast.Cast (bo, ty) -> add_level_info Ast.simple_prec Ast.simple_assoc (hvbox false true [ - builtin_symbol "("; k bo; break; builtin_symbol ":"; k ty; - builtin_symbol ")"]) + builtin_symbol "("; top_pos (k bo); break; builtin_symbol ":"; + top_pos (k ty); builtin_symbol ")"]) | Ast.LetIn (var, s, t) -> add_level_info Ast.let_in_prec Ast.let_in_assoc (hvbox false true [ hvbox false true [ keyword "let"; hvbox false true [ - aux_var var; builtin_symbol "\\def"; break; k s ]; + aux_var var; builtin_symbol "\\def"; break; top_pos (k s) ]; break; keyword "in" ]; break; k t ]) @@ -218,7 +245,7 @@ let pp_ast0 t k = let (name, body) = fst_fun in hvbox false true [ keyword "let"; keyword rec_op; name; builtin_symbol "\\def"; break; - body ] + top_pos body ] in let tl_rows = List.map @@ -271,13 +298,14 @@ let pp_ast0 t k = 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 + let id_to_uris = term_info.uri in + let register_uri id uri = Hashtbl.add id_to_uris id uri in let sort_of_id id = try Hashtbl.find term_info.sort id with Not_found -> prerr_endline (sprintf "warning: sort of id %s not found, using Type" id); - `Type + `Type (CicUniv.fresh ()) in let aux_substs substs = Some @@ -295,18 +323,19 @@ let ast_of_acic0 term_info acic k = let aux = function | Cic.ARel (id,_,_,b) -> idref id (Ast.Ident (b, None)) | Cic.AVar (id,uri,substs) -> - register_uri id (UriManager.string_of_uri uri); + register_uri id uri; idref id (Ast.Ident (UriManager.name_of_uri uri, aux_substs substs)) | Cic.AMeta (id,n,l) -> idref id (Ast.Meta (n, aux_context l)) | Cic.ASort (id,Cic.Prop) -> idref id (Ast.Sort `Prop) | Cic.ASort (id,Cic.Set) -> idref id (Ast.Sort `Set) - | Cic.ASort (id,Cic.Type _) -> idref id (Ast.Sort `Type) + | Cic.ASort (id,Cic.Type u) -> idref id (Ast.Sort (`Type u)) | Cic.ASort (id,Cic.CProp) -> idref id (Ast.Sort `CProp) - | Cic.AImplicit _ -> assert false + | Cic.AImplicit (id, Some `Hole) -> idref id Ast.UserInput + | Cic.AImplicit (id, _) -> idref id Ast.Implicit | Cic.AProd (id,n,s,t) -> let binder_kind = match sort_of_id id with - | `Set | `Type -> `Pi + | `Set | `Type _ -> `Pi | `Prop | `CProp -> `Forall in idref id (Ast.Binder (binder_kind, @@ -320,19 +349,19 @@ let ast_of_acic0 term_info acic k = 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); + register_uri id uri; idref id (Ast.Ident (UriManager.name_of_uri uri, aux_substs 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 = sprintf "%s#xpointer(1/%d)" uri_str (i+1) in - register_uri id puri_str; + register_uri id (UriManager.uri_of_string 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; + register_uri id (UriManager.uri_of_string 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 @@ -353,12 +382,14 @@ let ast_of_acic0 term_info acic k = in let j = ref 0 in let patterns = - List.map2 - (fun (name, ty) pat -> - incr j; - let (capture_variables, rhs) = eat_branch ty pat in - ((name, Some (ctor_puri !j), capture_variables), rhs)) - constructors patterns + try + List.map2 + (fun (name, ty) pat -> + incr j; + let (capture_variables, rhs) = eat_branch ty pat in + ((name, Some (ctor_puri !j), capture_variables), rhs)) + constructors patterns + with Invalid_argument _ -> assert false in idref id (Ast.Case (k te, Some case_indty, Some (k ty), patterns)) | Cic.AFix (id, no, funs) -> @@ -418,29 +449,42 @@ let get_compiled32 () = 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 +let add_idrefs = + List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t)) + +let instantiate21 idrefs env l1 = + let rec subst_singleton pos env = + function + Ast.AttributedTerm (attr, t) -> + Ast.AttributedTerm (attr, subst_singleton pos env t) + | t -> CicNotationUtil.group (subst pos env t) + and subst pos env = function + | Ast.AttributedTerm (attr, t) as term -> +(* prerr_endline ("loosing attribute " ^ CicNotationPp.pp_attribute attr); *) + subst pos 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 + with Not_found -> + prerr_endline ("name " ^ name ^ " not found in environment"); + assert false in 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 -> [ (*reset_href*) (add_keyword_attrs t) ] - | Ast.Literal _ as t -> [ (*reset_href*) t ] - | Ast.Layout l -> [ Ast.Layout (subst_layout env l) ] - | t -> [ CicNotationUtil.visit_ast (subst_singleton env) t ] - and subst_magic env = function + [ add_pos_info pos (CicNotationEnv.term_of_value value) ] + | Ast.Magic m -> subst_magic pos env m + | Ast.Literal l as t -> + let t = add_idrefs idrefs t in + (match l with + | `Keyword k -> [ add_keyword_attrs t ] + | _ -> [ t ]) + | Ast.Layout l -> [ Ast.Layout (subst_layout pos env l) ] + | t -> [ CicNotationUtil.visit_ast (subst_singleton pos env) t ] + and subst_magic pos env = function | Ast.List0 (p, sep_opt) | Ast.List1 (p, sep_opt) -> let rec_decls = CicNotationEnv.declarations_of_term p in @@ -457,11 +501,12 @@ let instantiate21 env (* precedence associativity *) l1 = | [] -> List.rev acc | value_set :: [] -> let env = CicNotationEnv.combine rec_decls value_set in - instantiate_list (CicNotationUtil.group (subst env p) :: acc) [] + instantiate_list (CicNotationUtil.group (subst pos 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 + let terms = subst pos env p in + instantiate_list (CicNotationUtil.group (terms @ sep) :: acc) tl in instantiate_list [] values | Ast.Opt p -> @@ -480,15 +525,37 @@ let instantiate21 env (* precedence associativity *) l1 = begin match env with | [] -> [] - | _ -> subst env p + | _ -> subst pos env p end | _ -> assert false (* impossible *) - and subst_layout env = function + and subst_layout pos env = function | Ast.Box (kind, tl) -> - Ast.Box (kind, List.concat (List.map (subst env) tl)) - | l -> CicNotationUtil.visit_layout (subst_singleton env) l + let tl' = subst_children pos env tl in + Ast.Box (kind, List.concat tl') + | l -> CicNotationUtil.visit_layout (subst_singleton pos env) l + and subst_children pos env = + function + | [] -> [] + | [ child ] -> + let pos' = + match pos with + | `Inner -> `Right + | `Left -> `Left +(* | `None -> assert false *) + | `Right -> `Right + in + [ subst pos' env child ] + | hd :: tl -> + let pos' = + match pos with + | `Inner -> `Inner + | `Left -> `Inner +(* | `None -> assert false *) + | `Right -> `Right + in + (subst pos env hd) :: subst_children pos' env tl in - subst_singleton env l1 + subst_singleton `Left env l1 let rec pp_ast1 term = let rec pp_value = function @@ -505,24 +572,30 @@ let rec pp_ast1 term = let ast_env_of_env env = List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env in +(* prerr_endline ("pattern matching from 2 to 1 on term " ^ CicNotationPp.pp_term term); *) match term with - | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, pp_ast1 t) + | Ast.AttributedTerm (attrs, term') -> + Ast.AttributedTerm (attrs, pp_ast1 term') | _ -> (match (get_compiled21 ()) term with | None -> pp_ast0 term pp_ast1 - | Some (env, pid) -> - let prec, assoc, l1 = + | Some (env, ctors, pid) -> + let idrefs = + List.flatten (List.map CicNotationUtil.get_idrefs ctors) + in + let l1 = try Hashtbl.find level1_patterns21 pid with Not_found -> assert false in - add_level_info prec assoc (instantiate21 (ast_env_of_env env) l1)) + instantiate21 idrefs (ast_env_of_env env) l1) -let instantiate32 term_info env symbol args = +let instantiate32 term_info idrefs env symbol args = let rec instantiate_arg = function | Ast.IdentArg (n, name) -> let t = (try List.assoc name env with Not_found -> assert false) in let rec count_lambda = function + | Ast.AttributedTerm (_, t) -> count_lambda t | Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body | _ -> 0 in @@ -536,44 +609,62 @@ let instantiate32 term_info env symbol args = in add_lambda t (n - count_lambda t) in - let head = Ast.Symbol (symbol, 0) in - match args with - | [] -> head - | _ -> Ast.Appl (head :: List.map instantiate_arg args) + let head = + let symbol = Ast.Symbol (symbol, 0) in + add_idrefs idrefs symbol + in + if args = [] then head + else Ast.Appl (head :: List.map instantiate_arg args) let rec ast_of_acic1 term_info annterm = + let id_to_uris = term_info.uri in + let register_uri id uri = Hashtbl.add id_to_uris id uri in match (get_compiled32 ()) annterm with | None -> ast_of_acic0 term_info annterm ast_of_acic1 - | Some (env, pid) -> + | Some (env, ctors, pid) -> + let idrefs = + List.map + (fun annterm -> + let idref = CicUtil.id_of_annterm annterm in + (try + register_uri idref + (CicUtil.uri_of_term (Deannotate.deannotate_term annterm)) + with Invalid_argument _ -> ()); + idref) + ctors + in let env' = List.map (fun (name, term) -> (name, ast_of_acic1 term_info term)) env in - let _, symbol, args, _, uris = + let _, symbol, args, _ = try Hashtbl.find level2_patterns32 pid with Not_found -> assert false in - let ast = instantiate32 term_info env' symbol args in - Ast.AttributedTerm (`IdRef (CicUtil.id_of_annterm annterm), - (match uris with - | [] -> ast - | _ -> Ast.AttributedTerm (`Href uris, ast))) + let ast = instantiate32 term_info idrefs env' symbol args in + Ast.AttributedTerm (`IdRef (CicUtil.id_of_annterm annterm), ast) let load_patterns32 t = + let t = + HExtlib.filter_map (function (true, ap, id) -> Some (ap, id) | _ -> None) t + in 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 = + 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 term_info annterm in - debug_print ("ast_of_acic -> " ^ CicNotationPp.pp_term ast); + debug_print (lazy ("ast_of_acic -> " ^ CicNotationPp.pp_term ast)); ast, term_info.uri let pp_ast ast = + debug_print (lazy "pp_ast <-"); let ast' = pp_ast1 ast in - debug_print ("pp_ast -> " ^ CicNotationPp.pp_term ast'); + debug_print (lazy ("pp_ast -> " ^ CicNotationPp.pp_term ast')); ast' let fresh_id = @@ -584,9 +675,8 @@ let fresh_id = let add_interpretation dsc (symbol, args) appl_pattern = let id = fresh_id () in - let uris = CicNotationUtil.find_appl_pattern_uris appl_pattern in - Hashtbl.add level2_patterns32 id (dsc, symbol, args, appl_pattern, uris); - pattern32_matrix := (appl_pattern, id) :: !pattern32_matrix; + 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 @@ -594,6 +684,32 @@ let add_interpretation dsc (symbol, args) appl_pattern = 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 exception Pretty_printer_not_found @@ -609,7 +725,7 @@ let lookup_interpretations symbol = (List.sort Pervasives.compare (List.map (fun id -> - let (dsc, _, args, appl_pattern, _) = + let (dsc, _, args, appl_pattern) = try Hashtbl.find level2_patterns32 id with Not_found -> assert false @@ -618,22 +734,37 @@ let lookup_interpretations symbol = !(Hashtbl.find interpretations symbol))) with Not_found -> raise Interpretation_not_found +let fill_pos_info l1_pattern = l1_pattern +(* let rec aux toplevel pos = + function + | Ast.Layout l -> + (match l + + | Ast.Magic m -> + Ast.Box ( + | Ast.Variable _ as t -> add_pos_info pos t + | t -> t + in + aux true l1_pattern *) + let add_pretty_printer ~precedence ~associativity l2 l1 = let id = fresh_id () in + let l1' = add_level_info precedence associativity (fill_pos_info l1) in let l2' = CicNotationUtil.strip_attributes l2 in - Hashtbl.add level1_patterns21 id (precedence, associativity, l1); + Hashtbl.add level1_patterns21 id l1'; pattern21_matrix := (l2', id) :: !pattern21_matrix; load_patterns21 !pattern21_matrix; id let remove_interpretation id = (try - let _, symbol, _, _, _ = Hashtbl.find level2_patterns32 id in + let _, 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; + pattern32_matrix := + List.filter (fun (_, _, id') -> id <> id') !pattern32_matrix; load_patterns32 !pattern32_matrix let remove_pretty_printer id =