]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationRew.ml
version 0.7.1
[helm.git] / helm / ocaml / cic_notation / cicNotationRew.ml
index ec385efcef8507c64ef35a1c693b3d4676ce4633..2f95a56350f5af1b5fa492c36d2310fa18debb18 100644 (file)
@@ -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
@@ -77,6 +62,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
@@ -86,11 +72,41 @@ 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 pp_ast0 t k =
-  prerr_endline "pp_ast0";
-  let rec aux t = CicNotationUtil.visit_ast ~special_k k t
+  let rec aux = function
+    | Ast.Appl ts ->
+        Ast.AttributedTerm (`Level (Parser.apply_prec, Parser.apply_assoc),
+          Ast.Layout (Ast.Box ((Ast.HOV, true, true), 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.Box ((Ast.H, false, false), [
+              Ast.Literal (`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), [
+            Ast.Layout (Ast.Box ((Ast.H, false, false), [
+              Ast.Literal (`Symbol (resolve_binder binder_kind));
+              k id;
+              Ast.Literal (`Symbol ":");
+              aux_ty ty ]));
+            Ast.Layout (Ast.Box ((Ast.H, false, false), [
+              Ast.Literal (`Symbol ".");
+              k body ]))])))
+    | t -> CicNotationUtil.visit_ast ~special_k k t
+  and aux_ty = function
+    | None -> Ast.Literal (`Symbol "?")
+    | Some ty -> k ty
   and special_k = function
-    | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, aux t)
+    | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, k t)
     | _ -> assert false
   in
   aux t
@@ -212,218 +228,35 @@ 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:
-   *   <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
-          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 =
-  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 instantiate21 env precedence associativity l1 =
+  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 +268,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 +339,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 +401,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 +419,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 +435,5 @@ let remove_pretty_printer id =
 
 let _ =
   load_patterns21 [];
-(*   load_patterns32 [] *)
+  load_patterns32 []