X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationRew.ml;h=151ec8a08516cf8074fe6aad4483a662be46d0ff;hb=ec54d490477ece51c19d79750dda9805ffda663c;hp=ec385efcef8507c64ef35a1c693b3d4676ce4633;hpb=50377dde5b5b1a8e5c7b2fb48b47defde9508b50;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index ec385efce..151ec8a08 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -36,21 +36,6 @@ type term_info = let warning s = prerr_endline ("CicNotation WARNING: " ^ s) -(* module Pattern32 = - struct - type pattern_t = CicNotationPt.cic_appl_pattern - let compatible ap1 ap2 = - match ap1, ap2 with - | CicNotationPt.UriPattern _, CicNotationPt.UriPattern _ - | CicNotationPt.ArgPattern _, CicNotationPt.ArgPattern _ - | CicNotationPt.ApplPattern _, CicNotationPt.ApplPattern _ -> true - | _ -> false - end - -module Patterns32 = Patterns (Pattern32) *) - - (* acic -> ast auxiliary function s *) - let get_types uri = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with @@ -212,218 +197,36 @@ let ast_of_acic0 term_info acic k = (* persistent state *) let level1_patterns21 = Hashtbl.create 211 -(* let level2_patterns32 = Hashtbl.create 211 *) +let level2_patterns32 = Hashtbl.create 211 -let (compiled21: (CicNotationPt.term -> (CicNotationEnv.t * pattern_id) option) +let (compiled21: (CicNotationPt.term -> (CicNotationEnv.t * int) option) +option ref) = + ref None +let (compiled32: (Cic.annterm -> ((string * Cic.annterm) list * int) option) option ref) = ref None -(* let (compiled32: (term_info -> Cic.annterm -> CicNotationPt.term) option ref) = - ref None *) let pattern21_matrix = ref [] -(* let pattern32_matrix = ref Patterns32.empty *) +let pattern32_matrix = ref [] let get_compiled21 () = match !compiled21 with | None -> assert false | Some f -> f -(* let get_compiled32 () = +let get_compiled32 () = match !compiled32 with | None -> assert false - | Some f -> f *) + | Some f -> f let set_compiled21 f = compiled21 := Some 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 - success_k term_info (List.hd envl) - with Failure _ -> assert false) - | _ -> assert false) - -let variable_closure names k = - (fun term_info terms envl -> -(* prerr_endline "variable_closure"; *) - 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 (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 (id, 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 -> -(* prerr_endline "appl_closure"; *) - (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 -> -(* 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 - 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: Patterns32.t) success_k fail_k = - let rec aux t k = |+ k is a continuation +| - if t = [] then - k - else if Patterns32.are_empty t then begin - (match t with - | _::_::_ -> - |+ XXX optimization possible here: throw away all except one of the - * rules which lead to ambiguity +| - warning "ambiguous interpretation" - | _ -> ()); - return_closure success_k - end else - match Patterns32.horizontal_split t with - | t', [] -> - (match t' with - | [] - | ([], _) :: _ -> assert false - | (Ast.ArgPattern (Ast.IdentArg _) :: _, _) :: _ - | (Ast.ArgPattern (Ast.EtaArg _) :: _, _) :: _ -> - let first_column, t'' = Patterns32.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 = Patterns32.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 = Patterns32.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) - -let ast_of_acic1 term_info annterm = (get_compiled32 ()) term_info annterm *) +let set_compiled32 f = compiled32 := Some f -let instantiate21 env pid = +let instantiate21 env precedence associativity l1 = prerr_endline "instantiate21"; - let precedence, associativity, l1 = - try - Hashtbl.find level1_patterns21 pid - with Not_found -> assert false - in - let rec subst = function - | Ast.AttributedTerm (_, t) -> subst t + let rec subst_singleton env t = + CicNotationUtil.boxify (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 = @@ -435,13 +238,60 @@ let instantiate21 env pid = (* 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 _ -> assert false (* TO BE IMPLEMENTED *) - | Ast.Literal _ as t -> t - | Ast.Layout l -> Ast.Layout (subst_layout l) - | t -> CicNotationUtil.visit_ast subst t - and subst_layout l = CicNotationUtil.visit_layout subst l in - subst l1 + [ CicNotationEnv.term_of_value value ] + | Ast.Magic m -> subst_magic env m + | 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.boxify (subst env p)) :: acc) [] + | value_set :: tl -> + let env = CicNotationEnv.combine rec_decls value_set in + instantiate_list + ((CicNotationUtil.boxify (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 + subst_singleton env l1 let rec pp_ast1 term = let rec pp_value = function @@ -459,65 +309,59 @@ let rec pp_ast1 term = in match (get_compiled21 ()) term with | None -> pp_ast0 term pp_ast1 - | Some (env, pid) -> instantiate21 (ast_env_of_env env) pid - -(* let instantiate32 term_info name_env term_env pid = - let symbol, args = - try - Hashtbl.find level2_patterns32 pid - with Not_found -> assert false - in + | Some (env, pid) -> + let precedence, associativity, l1 = + try + Hashtbl.find level1_patterns21 pid + with Not_found -> assert false + in + instantiate21 (ast_env_of_env env) precedence associativity l1 + +let instantiate32 term_info env symbol args = 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 + | Ast.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 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)) + 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 = + try + Hashtbl.find level2_patterns32 pid + with Not_found -> assert false + in + instantiate32 term_info env' symbol args + let load_patterns32 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, id) -> Some (ast_of_acic1 term_info annterm, id) - in - (name, (name', ast_ty_opt))) - name_env - in - let ast_env_of_term_env term_info = - List.map (fun (name, term) -> (name, ast_of_acic1 term_info term)) - 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) = - instantiate32 - term_info - (ast_env_of_name_env term_info name_env) - (ast_env_of_term_env term_info term_env) - pid - in - let compiled32 = compiler32 t success_k fail_k in - set_compiled32 compiled32 *) + set_compiled32 (CicNotationMatcher.Matcher32.compiler t) let load_patterns21 t = - set_compiled21 (CicNotationMatcher.T21.compiler t) + set_compiled21 (CicNotationMatcher.Matcher21.compiler t) -(* let ast_of_acic id_to_sort annterm = +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 *) + ast, term_info.uri let pp_ast term = pp_ast1 term @@ -527,12 +371,12 @@ let fresh_id = incr counter; !counter -(* let add_interpretation (symbol, args) appl_pattern = +let add_interpretation (symbol, args) appl_pattern = let id = fresh_id () in Hashtbl.add level2_patterns32 id (symbol, args); - pattern32_matrix := ([appl_pattern], id) :: !pattern32_matrix; + pattern32_matrix := (appl_pattern, id) :: !pattern32_matrix; load_patterns32 !pattern32_matrix; - id *) + id let add_pretty_printer ?precedence ?associativity l2 l1 = let id = fresh_id () in @@ -545,12 +389,12 @@ let add_pretty_printer ?precedence ?associativity l2 l1 = exception Interpretation_not_found exception Pretty_printer_not_found -(* let remove_interpretation id = +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 *) + load_patterns32 !pattern32_matrix let remove_pretty_printer id = (try @@ -561,5 +405,5 @@ let remove_pretty_printer id = let _ = load_patterns21 []; -(* load_patterns32 [] *) + load_patterns32 []