1. Peter_Sewell
  2. lem

Commits

Thomas Tuerk  committed 4a3b4fa

fix name resolution of Id_none

Ids carry either an identifier via "Id_some i" (usually as the user typed it)
or have a "Id_none" entry (if generated by some macro).
"Id_none" needs resolving into an suitable identifier. This identifier depends on the local
context. Unluckily the local context was not available. This commit adds a local context to
definitions. This context is then be used by the backends to figure out suitable identifiers.

  • Participants
  • Parent commits fd388de
  • Branches master

Comments (0)

Files changed (34)

File src/backend.ml

View file
  • Ignore whitespace
   let module_end = kwd "end"
   let module_open = kwd "open"
 
-  let some = Ident.mk_ident [] (Name.add_lskip (Name.from_rope (r"Some"))) Ast.Unknown
-  let none = Ident.mk_ident [] (Name.add_lskip (Name.from_rope (r"None"))) Ast.Unknown
-  let inl = Ident.mk_ident [] (Name.add_lskip (Name.from_rope (r"Inl"))) Ast.Unknown
-  let inr = Ident.mk_ident [] (Name.add_lskip (Name.from_rope (r"Inr"))) Ast.Unknown
+  let some = Ident.mk_ident_strings [] "Some"
+  let none = Ident.mk_ident_strings [] "None"
+  let inl = Ident.mk_ident_strings [] "Inl"
+  let inr = Ident.mk_ident_strings [] "Inr"
 end
 
 module Html : Target = struct
   let module_end = tkwdr "end"
   let module_open = tkwdl "open"
 
-  let some = Ident.mk_ident [] (Name.add_lskip (Name.from_rope (r"Some"))) Ast.Unknown
-  let none = Ident.mk_ident [] (Name.add_lskip (Name.from_rope (r"None"))) Ast.Unknown
-  let inl = Ident.mk_ident [] (Name.add_lskip (Name.from_rope (r"Inl"))) Ast.Unknown
-  let inr = Ident.mk_ident [] (Name.add_lskip (Name.from_rope (r"Inr"))) Ast.Unknown
+  let some = Ident.mk_ident_strings [] "Some"
+  let none = Ident.mk_ident_strings [] "None"
+  let inl = Ident.mk_ident_strings [] "Inl"
+  let inr = Ident.mk_ident_strings [] "Inr"
 end
 
 
   let type_params_pre = true
   let nexp_params_vis = false
   
-  let inl = Ident.mk_ident [] (Name.add_lskip (Name.from_rope (r"Inl"))) Ast.Unknown
-  let inr = Ident.mk_ident [] (Name.add_lskip (Name.from_rope (r"Inr"))) Ast.Unknown
+  let inl = Ident.mk_ident_strings [] "Inl"
+  let inr = Ident.mk_ident_strings [] "Inr"
 end
 
 let back_tick = List.hd (Ulib.Text.explode (r"`"))
   let module_end = kwd "end"
   let module_open = kwd "open"
 
-  let some = Ident.mk_ident [] (Name.add_lskip (Name.from_rope (r"SOME"))) Ast.Unknown
-  let none = Ident.mk_ident [] (Name.add_lskip (Name.from_rope (r"NONE"))) Ast.Unknown
-  let inl = Ident.mk_ident [] (Name.add_lskip (Name.from_rope (r"INL"))) Ast.Unknown
-  let inr = Ident.mk_ident [] (Name.add_lskip (Name.from_rope (r"INR"))) Ast.Unknown
-
+  let some = Ident.mk_ident_strings [] "SOME"
+  let none = Ident.mk_ident_strings [] "NONE"
+  let inl = Ident.mk_ident_strings [] "INL"
+  let inr = Ident.mk_ident_strings [] "INR"
 end
 
 
-module F(T : Target)(A : sig val avoid : var_avoid_f option;; val env : env end)(X : sig val comment_def : def -> Ulib.Text.t end) = struct
+(* which extra information should be generated? *)
+type extra_gen_flags = 
+   {extra_gen_termination: bool; 
+    extra_gen_asserts: bool;
+    extra_gen_lemmata: bool;
+    extra_gen_theorems: bool;
+};;
+
+let extra_gen_flags_gen_lty (gf : extra_gen_flags) = function
+  | Ast.Lemma_theorem _ -> gf.extra_gen_theorems
+  | Ast.Lemma_lemma _ -> gf.extra_gen_lemmata
+  | Ast.Lemma_assert _ -> gf.extra_gen_asserts
+
+
+module F_Aux(T : Target)(A : sig val avoid : var_avoid_f option;; val env : env end)(X : sig val comment_def : def -> Ulib.Text.t end) = struct
 
 module B = Backend_common.Make (struct
   let env = A.env
       ws s ^ id Nexpr_var (Ulib.Text.(^^^) T.nexp_var (Nvar.to_rope n))
 
   | Constant(cd) ->
-      Output.concat emp (B.function_application_to_output exp false cd [])
+      Output.concat emp (B.function_application_to_output (exp_to_locn e) exp false e cd [])
 
   | Fun(s1,ps,s2,e) ->
       ws s1 ^
          match C.exp_to_term e0 with
            | Constant cd -> 
              (* constant, so use special formatting *)
-             B.function_application_to_output trans false cd args
+             B.function_application_to_output (exp_to_locn e) trans false e cd args
            | _ -> (* no constant, so use standard one *)
              List.map trans (e0 :: args)
       end in
          match C.exp_to_term e2 with
            | Constant cd -> 
              (* constant, so use special formatting *)
-             B.function_application_to_output trans true cd [e1;e3]
+             B.function_application_to_output (exp_to_locn e) trans true e cd [e1;e3]
            | _ -> (* no constant, so use standard one *)
              List.map trans [e1;e2;e3]
       end in
   | Do(s1,m,do_lns,s2,e,s3,_) ->
       ws s1 ^
       kwd "do" ^
-      Ident.to_output Module_name T.path_sep (resolve_ident_path m m.descr.mod_binding) ^
+      Ident.to_output Module_name T.path_sep (B.module_id_to_ident m) ^
       do_lines do_lns ^
       ws s2 ^
       kwd "in" ^
     | (_,_,_,Te_record _,_) -> true
     | _ -> false
 
-(* which extra information should be generated? *)
-type extra_gen_flags = 
-   {extra_gen_termination: bool; 
-    extra_gen_asserts: bool;
-    extra_gen_lemmata: bool;
-    extra_gen_theorems: bool;
-};;
-
-let extra_gen_flags_gen_lty (gf : extra_gen_flags) = function
-  | Ast.Lemma_theorem _ -> gf.extra_gen_theorems
-  | Ast.Lemma_lemma _ -> gf.extra_gen_lemmata
-  | Ast.Lemma_assert _ -> gf.extra_gen_asserts
-
 let rec isa_def_extra (gf:extra_gen_flags) d l : Output.t = match d with
   | Val_def(Fun_def(s1, s2_opt, targets, clauses),tnvs, class_constraints) 
       when gf.extra_gen_termination -> 
-      let (_, is_rec) = Typed_ast_syntax.is_recursive_def ((d, None), Ast.Unknown) in
+      let (_, is_rec) = Typed_ast_syntax.is_recursive_def d in
       if (in_target targets && is_rec) then
       begin
         let n = 
 let rec hol_def_extra gf d l : Output.t = match d with
   | Val_def(Fun_def(s1, s2_opt, targets, clauses),tnvs, class_constraints) 
       when gf.extra_gen_termination -> 
-      let (_, is_rec) = Typed_ast_syntax.is_recursive_def ((d, None), Ast.Unknown) in
+      let (_, is_rec) = Typed_ast_syntax.is_recursive_def d in
       if (in_target targets && is_rec) then
       begin
         let n = 
   | _ -> emp
 
 
-let rec def d is_user_def : Output.t = match d with
+let rec def_internal callback (inside_module : bool) d is_user_def : Output.t = match d with
 
   (* A single type abbreviation *)
   | Type_def(s1, l) when is_abbrev l->
         emp
   | Val_def(Fun_def(s1, s2_opt, targets, clauses),tnvs, class_constraints) -> 
       if in_target targets then
-        let (is_rec, is_real_rec) = Typed_ast_syntax.is_recursive_def ((d, None), Ast.Unknown) in
+        let (is_rec, is_real_rec) = Typed_ast_syntax.is_recursive_def d in
         let s2 = Util.option_default None s2_opt in
         let n = 
           match Seplist.to_list clauses with
       kwd "=" ^
       ws s3 ^
       T.module_struct ^
-      defs ds ^
+      callback ds ^
       ws s4 ^
       T.module_end
   | Rename(s1,(n,l),mod_bind,s2,m) ->
       Name.to_output Module_name n ^
       ws s2 ^
       kwd "=" ^
-      Ident.to_output Module_name T.path_sep (resolve_ident_path m m.descr.mod_binding)
+      Ident.to_output Module_name T.path_sep (B.module_id_to_ident m)
   | Open(s,m) ->
       ws s ^
       T.module_open ^
-      Ident.to_output Module_name T.path_sep (resolve_ident_path m m.descr.mod_binding)
+      Ident.to_output Module_name T.path_sep (B.module_id_to_ident m)
   | Indreln(s,targets,clauses) ->
       if in_target targets then
         ws s ^
       typ t ^
       ws s3 ^
       kwd ")" ^
-      flat (List.map (fun d -> def (Val_def(d,Types.TNset.empty,[])) is_user_def) methods) ^
+      flat (List.map (fun d -> def callback true (Val_def(d,Types.TNset.empty,[])) is_user_def) methods) ^
       ws s4 ^
       kwd "end"
   | Class(s1,s2,(n,l), tv, class_path, s3, specs, s4) -> 
   print in whole-document mode (minus the "\lemdef" there).  Modulo the pre/post comments...
 *)
 
+and (^^^^) = Ulib.Text.(^^^)
 
 and make_lemdefn latex_name latex_label typeset_name pre_comment lhs_keyword lhs rhs post_comment = 
   (r"\\newcommand{" ^^^^ latex_name ^^^^ r"}{%\n" ^^^^
 
 
 (* keep locations for latex-name-clash error reporting... *)
-
 and names_of_pat p : (Ulib.Text.t * Ulib.Text.t * Ast.l) list = match p.term with
   | P_wild(s) ->
       []
       []
 
 
-and tex_of_output out = 
-  match to_rope_option_tex T.lex_skip T.need_space true out with
-  | None -> r""
-  | Some r -> r
-
+and tex_of_output out = to_rope_tex out
 
 and tex_inc_letbind (p, name_map, topt, sk, e) lhs_keyword = 
       let (source_name, typeset_name) = 
 
 
 and def_tex_inc d : (Ulib.Text.t*Ulib.Text.t) list = match d with
-
-(*   (\* A single type abbreviation *\) *)
-(*   | Type_def(s1, l) when is_abbrev l-> *)
-(*       begin *)
-(*         match Seplist.hd l with *)
-(*           | (s2,tvs,s3,(n,l),Te_abbrev(s4,t)) -> *)
-(*               ws s1 ^ *)
-(*               T.type_abbrev_start ^ *)
-(*               tdef_tctor T.type_abbrev_name_quoted s2 tvs s3 n ^ *)
-(*               tyexp_abbrev s4 t ^ *)
-(*               T.type_abbrev_end *)
-(*           | _ -> assert false *)
-(*       end *)
-
-(*   (\* A single record definition *\) *)
-(*   | Type_def(s1, l) when is_rec l-> *)
-(*       begin *)
-(*         match Seplist.hd l with *)
-(*           | (s2,tvs,s3,(n,l),Te_record(s4,s5,fields,s6)) -> *)
-(*               ws s1 ^ *)
-(*               T.typedefrec_start ^ *)
-(*               tdef_tctor false s2 tvs s3 n ^ *)
-(*               tyexp_rec s4 s5 fields s6 ^ *)
-(*               T.typedefrec_end *)
-(*           | _ -> assert false *)
-(*       end *)
-
-(*   | Type_def(s, defs) -> *)
-(*       ws s ^ *)
-(*       T.typedef_start ^ *)
-(*       flat (Seplist.to_sep_list tdef (sep T.typedef_sep) defs) ^ *)
-(*       T.typedef_end *)
-
   | Val_def(Let_def(s1, targets,bind),tnvs,class_constraints) ->
       if in_target targets then
         let lhs_keyword = tex_of_output (ws s1 ^ T.def_start) in
         [tex_inc_letbind bind lhs_keyword]
       else
         []
-
-
   | _ -> []
 
-(*   | Module(s1,(n,l),s2,s3,ds,s4) ->  *)
-(*       ws s1 ^ *)
-(*       T.module_module ^ *)
-(*       Name.to_output Module_name n ^ *)
-(*       ws s2 ^ *)
-(*       kwd "=" ^ *)
-(*       ws s3 ^ *)
-(*       T.module_struct ^ *)
-(*       defs ds ^ *)
-(*       ws s4 ^ *)
-(*       T.module_end *)
-(*   | Rename(s1,(n,l),s2,m) -> *)
-(*       ws s1 ^ *)
-(*       T.module_module ^ *)
-(*       Name.to_output Module_name n ^ *)
-(*       ws s2 ^ *)
-(*       kwd "=" ^ *)
-(*       Ident.to_output Module_name T.path_sep m.id_path *)
-(*   | Open(s,m) -> *)
-(*       ws s ^ *)
-(*       T.module_open ^ *)
-(*       Ident.to_output Module_name T.path_sep m.id_path *)
-(*   | Indreln(s,targets,clauses) -> *)
-(*       if in_target targets then *)
-(*         ws s ^ *)
-(*         T.reln_start ^ *)
-(*         (if T.target = None then *)
-(*            targets_opt targets  *)
-(*          else *)
-(*            emp) ^ *)
-(*         flat (Seplist.to_sep_list indreln_clause (sep T.reln_sep) clauses) ^ *)
-(*         T.reln_end *)
-(*       else *)
-(*         emp *)
-(*   | Val_spec(s1,(n,l),s2,(constraint_pre,t)) -> *)
-(*       ws s1 ^ *)
-(*       kwd "val" ^ *)
-(*       Name.to_output Term_var n ^ *)
-(*       ws s2 ^ *)
-(*       T.typ_sep ^ *)
-(*       begin *)
-(*         match constraint_pre with *)
-(*           | None -> emp *)
-(*           | Some(cp) -> constraint_prefix cp *)
-(*       end ^ *)
-(*       typ t *)
-(*   | Subst(s1,s2,target,s3,n,args,s4,body) -> *)
-(*       if (T.target = None) then *)
-(*         ws s1 ^ *)
-(*         kwd "sub" ^ *)
-(*         ws s2 ^ *)
-(*         kwd "[" ^ *)
-(*         target_to_output Term_var target ^ *)
-(*         ws s3 ^ *)
-(*         kwd "]" ^ *)
-(*         Name.to_output Term_var n.term ^ *)
-(*         flat (List.map (fun n -> Name.to_output Term_var n.term) args) ^  *)
-(*         ws s4 ^ *)
-(*         kwd "=" ^ *)
-(*         exp body *)
-(*       else *)
-(*         emp *)
-(*   | Instance(s1,(cp,s2,id,t,s3),methods,s4) -> *)
-(*       ws s1 ^ *)
-(*       kwd "instance" ^ *)
-(*       begin *)
-(*         match cp with *)
-(*           | None -> emp *)
-(*           | Some(cp) -> constraint_prefix cp *)
-(*       end ^ *)
-(*       ws s2 ^ *)
-(*       kwd "(" ^ *)
-(*       Ident.to_output Term_method T.path_sep id ^ *)
-(*       typ t ^ *)
-(*       ws s3 ^ *)
-(*       kwd ")" ^ *)
-(*       flat (List.map (fun d -> def (Val_def(d))) methods) ^ *)
-(*       ws s4 ^ *)
-(*       kwd "end" *)
-(*   | Class(s1,s2,(n,l), tv, s3, specs, s4) ->  *)
-(*       ws s1 ^ *)
-(*       kwd "class" ^ *)
-(*       ws s2 ^ *)
-(*       kwd "(" ^ *)
-(*       Name.to_output Class_name n ^ *)
-(*       tyvar tv ^ *)
-(*       ws s3 ^ *)
-(*       kwd ")" ^ *)
-(*       flat (List.map  *)
-(*               (fun (s1,(n,l),s2,t) -> *)
-(*                 ws s1 ^ *)
-(*                 kwd "val" ^ *)
-(*                 Name.to_output Term_method n ^ *)
-(*                 ws s2 ^ *)
-(*                 kwd ":" ^ *)
-(*                 typ t) *)
-(*               specs) ^ *)
-(*       ws s4 ^ *)
-(*       kwd "end" *)
-
 
 and html_source_name_letbind (p, _, _, _, _) = 
     match names_of_pat p with 
       | (source_name, typeset_name, l)::_ -> Some source_name
       | [] -> None
 
-and html_source_name_def d = match d with
+and html_source_name_def (d : def_aux) = match d with
   | Val_def(Let_def(s1, targets,bind),tnvs,class_constraints) ->
       html_source_name_letbind bind
   | _ -> None
   | Some s -> 
       let sr = Ulib.Text.to_string s in
       kwd ( String.concat "" ["\n<a name=\"";sr;"\">"])
-
-
-and defs (ds:def list) =
-  List.fold_right
-    (fun ((d,s),l) y -> 
-       begin
-         match T.target with 
-         | Target_no_ident Target_isa  -> isa_def d (is_trans_loc l)
-         | Target_no_ident Target_tex  -> raise (Failure "should be unreachable")
-         | Target_no_ident Target_html -> html_link_def d ^ def d (is_trans_loc l)
-         | _ -> def d (is_trans_loc l)
-       end ^
-
-       begin
-         match s with
-           | None ->
-               emp
-           | Some(s) -> 
-               ws s ^ kwd ";;"
-       end ^
-       y)
-    ds 
-    emp
-
-  
+ 
 (* Sets in Isabelle: the standard set notation only supports {x. P x} to define
  * a set, but for example not {f x. P x}. 
  * We use the Isabelle notation { f x | x. P x } to cope with that restriction.
  * So the general case {exp1|exp2} has to be translated to {exp1|Vars(exp1).exp2} *)
 (* TODO: try to move as much as possible to trans.ml and use normal def function *)
 
-and isa_def d is_user_def : Output.t = match d with 
+and isa_def callback inside_module d is_user_def : Output.t = match d with 
   | Type_def(s1, l) when is_abbrev l->
       begin
         match Seplist.hd l with
       else emp
   
   | Val_def (Fun_def (s1, s2_opt, targets, clauses),tnvs,class_constraints) ->
-      let (_, is_rec) = Typed_ast_syntax.is_recursive_def ((d, None), Ast.Unknown) in
+      let (_, is_rec) = Typed_ast_syntax.is_recursive_def d in
       if in_target targets then 
         let s2 = Util.option_default None s2_opt in
         ws s1 ^ kwd (if is_rec then "function (sequential)" else "fun") ^ ws s2 ^
       else
         emp
         
-  | _ -> def d is_user_def
+  | _ -> def callback inside_module d is_user_def
 
-  
-  (*
-        
-  | Module(s1,n,s2,s3,defs,s4) ->
-      raise (TODO "Isabelle Module Definition; should not occur at the moment")
+and def callback (inside_module : bool) d is_user_def =
+  match T.target with 
+   | Target_no_ident Target_isa  -> isa_def callback inside_module d is_user_def
+   | Target_no_ident Target_tex  -> 
+      meta "\\lemdef{\n" ^ def_internal callback inside_module d is_user_def ^ meta "\n}\n"
+   | Target_no_ident Target_html -> html_link_def d ^ def_internal callback inside_module d is_user_def
+   | _ -> def_internal callback inside_module d is_user_def
 
-  | Rename(s1,n,s2,m) ->
-      raise (TODO "Isabelle Renames; should not occur at the moment")
 
-  | Open(s,m) ->
-      raise (TODO "Isabelle Opens; should not occur at the moment")
+end
 
-  | Include(s,m) -> 
-      raise (TODO "Isabelle Includes; should not occur at the moment")
 
+module F(T : Target)(A : sig val avoid : var_avoid_f option;; val env : env end)(X : sig val comment_def : def -> Ulib.Text.t end) = struct
 
-  | Subst(s1,s2,target,s3,n,args,s4,body) -> 
-      raise (TODO "Isabelle substitution")    
+let (^^^^) = Ulib.Text.(^^^)
 
-*)
+let output_to_rope out = to_rope T.string_quote T.lex_skip T.need_space out
 
-(*********************)
+module F' = F_Aux(T)(A)(X)
 
-and (^^^^) = Ulib.Text.(^^^)
+module C = Exps_in_context (struct
+  let env_opt = Some A.env
+  let avoid = A.avoid
+end);;
 
-and to_rope_tex_def d : Ulib.Text.t = 
-  match to_rope_option_tex T.lex_skip T.need_space true (def d false) with
-  | None -> r""
-  | Some rr -> 
-      r"\\lemdef{\n" ^^^^
-      rr  ^^^^
-      r"\n}\n"
+let exp_to_rope e = output_to_rope (F'.exp e)
+let pat_to_rope p = output_to_rope (F'.pat p)
+let src_t_to_rope t = output_to_rope (F'.typ t)
+let typ_to_rope t = src_t_to_rope (C.t_to_src_t t)
+
+let rec batrope_pair_concat : (Ulib.Text.t * Ulib.Text.t) list -> (Ulib.Text.t * Ulib.Text.t)
+  = function
+    |  [] -> (r"",r"")
+    |  (r1,r2)::rrs  -> let (r1',r2') = batrope_pair_concat rrs in (r1^^^^r1', r2^^^^r2') 
+
+(* for -inc.tex file *)
+let defs_inc ((ds:def list),end_lex_skips) =
+  match T.target with
+  | Target_no_ident Target_tex -> 
+      batrope_pair_concat (List.map (function ((d,s),l,lenv) -> 
+        let module F' = F_Aux(T)(struct let avoid = A.avoid;; let env = { A.env with local_env = lenv } end)(X) in
+        batrope_pair_concat (F'.def_tex_inc d)) ds)
+  | _ ->
+      raise (Failure "defs_inc called on non-tex target")
 
-let output_to_rope out = to_rope T.string_quote T.lex_skip T.need_space out
+
+let rec defs (ds:def list) =
+  List.fold_right
+    (fun ((d,s),l,lenv) y -> 
+       begin
+        let module F' = F_Aux(T)(struct let avoid = A.avoid;; let env = { A.env with local_env = lenv } end)(X) in
+        F'.def defs false d (is_trans_loc l)
+       end ^
+
+       begin
+         match s with
+           | None ->
+               emp
+           | Some(s) -> 
+               ws s ^ kwd ";;"
+       end ^
+       y)
+    ds 
+    emp
+
+let defs_to_rope ((ds:def list),end_lex_skips) =
+  match T.target with
+  | Target_no_ident Target_tex -> 
+      (to_rope_tex (defs ds) ^^^^
+      (match to_rope_option_tex (ws end_lex_skips) with None -> r"" | Some rr -> 
+        r"\\lemdef{\n" ^^^^
+        rr  ^^^^
+        r"\n}\n"
+      ))
+  | _ -> output_to_rope (defs ds ^ ws end_lex_skips)
 
 let defs_to_extra_aux gf (ds:def list) =
     List.fold_right
-      (fun ((d,s),l) y -> 
+      (fun ((d,s),l,lenv) y -> 
          begin
+           let module F' = F_Aux(T)(struct let avoid = A.avoid;; let env = { A.env with local_env = lenv } end)(X) in
            match T.target with 
-           | Target_no_ident Target_isa   -> isa_def_extra gf d l 
-           | Target_no_ident Target_hol   -> hol_def_extra gf d l 
-           | Target_no_ident Target_ocaml -> ocaml_def_extra gf d l 
+           | Target_no_ident Target_isa   -> F'.isa_def_extra gf d l 
+           | Target_no_ident Target_hol   -> F'.hol_def_extra gf d l 
+           | Target_no_ident Target_ocaml -> F'.ocaml_def_extra gf d l 
            | _ -> emp
          end ^
 
     Some (output_to_rope (out ^ new_line ^ new_line))
 end
 
-let defs_to_rope ((ds:def list),end_lex_skips) =
-  match T.target with
-  | Target_no_ident Target_tex -> 
-      Ulib.Text.concat (r"") (List.map (function ((d,s),l) -> to_rope_tex_def d) ds) ^^^^
-      (match to_rope_option_tex T.lex_skip T.need_space true (ws end_lex_skips) with None -> r"" | Some rr -> 
-        r"\\lemdef{\n" ^^^^
-        rr  ^^^^
-        r"\n}\n"
-      )(* TODO*)
-  | _ ->
-      output_to_rope (defs ds ^ ws end_lex_skips)
-
-let exp_to_rope e = output_to_rope (exp e)
-let pat_to_rope p = output_to_rope (pat p)
-let src_t_to_rope t = output_to_rope (typ t)
-let typ_to_rope t = src_t_to_rope (C.t_to_src_t t)
-
-let rec batrope_pair_concat : (Ulib.Text.t * Ulib.Text.t) list -> (Ulib.Text.t * Ulib.Text.t)
-  = function
-    |  [] -> (r"",r"")
-    |  (r1,r2)::rrs  -> let (r1',r2') = batrope_pair_concat rrs in (r1^^^^r1', r2^^^^r2') 
-
-(* for -inc.tex file *)
-let defs_inc ((ds:def list),end_lex_skips) =
-  match T.target with
-  | Target_no_ident Target_tex -> 
-      batrope_pair_concat (List.map (function ((d,s),l) -> batrope_pair_concat (def_tex_inc d)) ds)
-  | _ ->
-      raise (Failure "defs_inc called on non-tex target")
-
-
-
 let header_defs ((defs:def list),(end_lex_skips : Typed_ast.lskips)) =  
   to_rope T.string_quote T.lex_skip T.need_space
     (List.fold_right 
-       (fun ((d,s),l) y ->
+       (fun ((d,s),l,lenv) y ->
+          let module B = Backend_common.Make (struct
+            let env = { A.env with local_env = lenv }
+            let target = T.target
+            let id_format_args =  (T.infix_op_format, T.path_sep)    
+          end) in
           begin match T.target with
 
               Target_no_ident Target_isa -> 
                 begin 
                   match d with 
                       Open(s,m) -> 
-                        kwd "\t \""^Ident.to_output Module_name T.path_sep (resolve_ident_path m m.descr.mod_binding)^kwd "\""
+                        kwd "\t \""^Ident.to_output Module_name T.path_sep (B.module_id_to_ident m)^kwd "\""
                     | _ -> emp
                 end
 
           y)
        defs 
        emp)
-
 end
 
 module Make(A : sig val avoid : var_avoid_f;; val env : env end) = struct

File src/backend_common.ml

View file
  • Ignore whitespace
 open Output
 open Typed_ast
 open Typed_ast_syntax
+open Target_binding
+
+let r = Ulib.Text.of_latin1
+let marker_lex_skip : Ast.lex_skips = (Some [Ast.Ws (Ulib.Text.of_latin1 "***marker***")])
+
+(* Resolve a const identifier stored inside a id, with a full one in case of Id_none *)
+let resolve_constant_id_ident env id path : Ident.t =
+  match id.id_path with 
+      | Id_none sk -> minimize_const_ident env (Path.to_ident sk path)
+      | Id_some id -> id
+
+let resolve_type_id_ident env id path : Ident.t =
+  match id.id_path with 
+      | Id_none sk -> minimize_type_ident env (Path.to_ident sk path)
+      | Id_some id -> id
+
+let resolve_module_id_ident env id path : Ident.t =
+  match id.id_path with 
+      | Id_none sk -> Path.to_ident sk (minimize_module_path env path)
+      | Id_some id -> id
+
+
+let cr_special_uncurry_fun n oL = begin
+  if not (List.length oL = n + 1) then
+     raise (Reporting_basic.Fatal_error (Reporting_basic.Err_internal (Ast.Unknown, "target presentation of OCaml constructor got the wrong number of args")))
+  else if (n = 0) then oL else
+  if (n = 1) then
+     [List.nth oL 0; texspace; List.nth oL 1]
+  else
+     [List.hd oL; texspace; meta "("] @
+      Util.intercalate (meta ",") (List.tl oL) @
+     [meta ")"]
+  end
+
+
+let cr_special_fun_to_fun = function
+  CR_special_uncurry n -> cr_special_uncurry_fun n
 
 
 (** Axiliary function for [inline_exp] *)
  end) = struct
 
 
+
+(** An auxiliary, temporary function to strip the artifacts of the library structure.
+    Hopefully, this won't be necessary much longer, when the library gets redesigned. *)
+let strip_library_prefix =
+  match A.target with
+    | Target.Target_ident -> (fun i -> i)
+    | Target.Target_no_ident t -> 
+         let n_t = Target.non_ident_target_to_mname t in
+         let n_p = Name.from_string "Pervasives" in
+      fun i -> begin
+         let i = Ident.strip_path n_t i in  
+(*         let i = Ident.strip_path n_p i in   *)
+         i
+      end
+
+
+(** TODO: add renaming of modules here later.
+          remove intermediate stripping of library prefix *)
+let fix_module_prefix_ident env i =
+  strip_library_prefix i
+
+
+
 let ident_to_output use_infix =
   let (ident_f, sep) = A.id_format_args in 
   if use_infix then
 let const_id_to_ident c_id =
   let l = Ast.Trans ("const_id_to_ident", None) in
   let c_descr = c_env_lookup l A.env.c_env c_id.descr in
+  let org_ident = resolve_constant_id_ident (A.env.local_env) c_id c_descr.const_binding in
   let i = match Target.Targetmap.apply_target c_descr.target_rep A.target with
-     | None -> resolve_ident_path c_id c_descr.const_binding
+     | None -> org_ident
      | Some (CR_new_ident (_, _, i)) -> i
-     | Some (CR_rename (_, _, n)) -> Ident.rename (resolve_ident_path c_id c_descr.const_binding) n
+     | Some (CR_rename (_, _, n)) -> Ident.rename org_ident n
      | Some (CR_inline _) -> raise (Reporting_basic.err_unreachable false l "Inlining should have already been done by Macro")
-     | Some (CR_special (_, _, _, n, _, _)) -> Ident.rename (resolve_ident_path c_id c_descr.const_binding) n
+     | Some (CR_special (_, _, _, n, _, _)) -> Ident.rename org_ident n
   in
-  i
+  let i' = fix_module_prefix_ident (A.env.local_env) i in
+  i'
 
 let constant_application_to_output_simple is_infix_pos arg_f args c_id = begin
   let i = const_id_to_ident c_id in 
   let is_infix = (is_infix_pos && const_is_infix && (Ident.has_empty_path_prefix i)) in
   let use_infix_notation = ((not is_infix) && const_is_infix) in
   let name = ident_to_output use_infix_notation i in
-  let args_out = List.map arg_f args in
+  let args_out = List.map (arg_f use_infix_notation) args in
   if (not is_infix) then
      (name :: args_out) 
   else 
   let name = ident_to_output false (const_id_to_ident c_id) in
   let args_output = List.map arg_f args in
   let (o_vars, o_rest) = Util.split_after (List.length vars) args_output (* assume there are enough elements *) in
-  let o_fun = to_out (name :: o_vars) in
+  let o_fun = (cr_special_fun_to_fun to_out) (name :: o_vars) in
   o_fun @ o_rest
 
 
-let function_application_to_output (arg_f : exp -> Output.t) (is_infix_pos : bool) (c_id : const_descr_ref id) (args : 'a list) : Output.t list =
+let function_application_to_output l (arg_f0 : exp -> Output.t) (is_infix_pos : bool) (full_exp : exp) (c_id : const_descr_ref id) (args : exp list) : Output.t list =
   let _ = if is_infix_pos && not (List.length args = 2) then (raise (Reporting_basic.err_unreachable false Ast.Unknown "Infix position with wrong number of args")) else () in
-
+  let arg_f b e = if b then arg_f0 (mk_opt_paren_exp e) else arg_f0 e in
   let c_descr = c_env_lookup Ast.Unknown A.env.c_env c_id.descr in
   match Target.Targetmap.apply_target c_descr.target_rep A.target with
      | Some (CR_special (_, _, _, _, to_out, vars)) -> 
             if (List.length args < List.length vars) then begin
-              raise (Reporting_basic.err_todo true Ast.Unknown "Special function syntax needs fun-introduction!")
+              (* eta expand and call recursively *)
+              let remaining_vars = Util.list_dropn (List.length args) vars in
+              let eta_exp = mk_eta_expansion_exp (A.env.t_env) remaining_vars full_exp in
+              [arg_f true eta_exp]
+              
             end else begin
-              constant_application_to_output_special c_id to_out arg_f args vars 
+              constant_application_to_output_special c_id to_out (arg_f false) args vars 
             end
      | _ -> constant_application_to_output_simple is_infix_pos arg_f args c_id
 
-let pattern_application_to_output (arg_f : pat -> Output.t) (c_id : const_descr_ref id) (args : pat list) : Output.t list =
+let pattern_application_to_output (arg_f0 : pat -> Output.t) (c_id : const_descr_ref id) (args : pat list) : Output.t list =
+  let arg_f b p = if b then arg_f0 (Pattern_syntax.mk_opt_paren_pat p) else arg_f0 p in
   let c_descr = c_env_lookup Ast.Unknown A.env.c_env c_id.descr in
   match Target.Targetmap.apply_target c_descr.target_rep A.target with
      | Some (CR_special (_, _, _, _, to_out, vars)) -> 
         if (List.length args < List.length vars) then begin
            raise (Reporting_basic.err_unreachable true Ast.Unknown "Constructor without enough arguments!")
         end else begin
-           constant_application_to_output_special c_id to_out arg_f args vars 
+           constant_application_to_output_special c_id to_out (arg_f false) args vars 
         end
      | _ -> constant_application_to_output_simple false arg_f args c_id
 
 let type_id_to_ident (p : Path.t id) =
    let l = Ast.Trans ("type_id_to_ident", None) in
    let td = Types.type_defs_lookup l A.env.t_env p.descr in
-   match Target.Targetmap.apply_target td.Types.type_target_rep A.target with
-     | None -> resolve_ident_path p p.descr
+   let org_type = resolve_type_id_ident A.env.local_env p p.descr in
+   let i = match Target.Targetmap.apply_target td.Types.type_target_rep A.target with
+     | None -> org_type
      | Some (Types.TR_new_ident (_, _, i)) -> i 
-     | Some (Types.TR_rename (_, _, n)) -> Ident.rename (resolve_ident_path p p.descr) n
-
-(* TODO: delete. Since type_ids are not implemente properly, drop everything except the name as a hack. Fix soon! *)
-let type_id_to_ident (p : Path.t id) =
-  Ident.drop_path (type_id_to_ident p)
-  
+     | Some (Types.TR_rename (_, _, n)) -> Ident.rename org_type n in
+   let i' = fix_module_prefix_ident A.env.local_env i in
+   i'
 
+let module_id_to_ident (mod_descr : mod_descr id) : Ident.t =
+   let l = Ast.Trans ("module_id_to_ident", None) in
+   let i = resolve_module_id_ident (A.env.local_env) mod_descr mod_descr.descr.mod_binding in
+   let i' = fix_module_prefix_ident (A.env.local_env) i in
+   i'
 
 let const_ref_to_name n0 c =
   let l = Ast.Trans ("const_ref_to_name", None) in

File src/backend_common.mli

View file
  • Ignore whitespace
 (** [inline_exp_macro target env e] does the inlining of target specific constant definitions *)
 val inline_exp_macro : Target.non_ident_target -> env -> exp -> exp option
 
-
 module Make(A : sig
   val env : env;; 
   val target : Target.target;;
   val id_format_args : (Output.id_annot -> Ulib.Text.t -> Output.t) * Output.t
  end) : sig
 
-(** [function_application_to_output exp inf c_id args] tries to format
-    a function application as output. It gets an id [c_id]. The
-    corresponding description is looked up in [A.env]. Depending on
+(** [function_application_to_output l exp inf full_exp c_id args] tries to format
+    a function application as output. It gets an expression [full_ex] of the from
+    [c arg1 ... argn]. The id [c_id] corresponds to constant [c]. The arguments [arg1, ... argn] are 
+    handed over as [args]. The description corresponding to [c] is looked up in [A.env]. Depending on
     this description and the backend-specific formats therein, the
     function and its arguments are formated as output.  In the
     simplest case the representation is an identifier ([Ident.t]),
     cases, formating of expressions is needed, which is done via the
     callback [exp]. In particular if some arguments are not needed by
     the formating of the function application, the function [exp] is
-    called on these remaining arguments.
+    called on these remaining arguments. The original expression [full_exp] is
+    needed, if not enough parameters are present to format the definition correctly. 
+    In this case, eta-expansion is applied and the resulting expression formatting via [exp].
 *)
-  val function_application_to_output : (exp -> Output.t) -> bool -> const_descr_ref id -> exp list -> Output.t list
+val function_application_to_output : Ast.l -> (exp -> Output.t) -> bool -> exp -> const_descr_ref id -> exp list -> Output.t list
 
 (** [pattern_application_to_output pat c_id args] tries to
     format a function application in a pattern as output. It does otherwise the same as
 *)
 val pattern_application_to_output : (pat -> Output.t) -> const_descr_ref id -> pat list -> Output.t list
 
-(** [const_id_to_ident c_id] tries to format a constant
+(** [const_id_to_ident c_id] tries to format a constant, constructor or field
     [c_id] as an identifier for target [A.target] using the rules stored
     in environment [A.env]. Depending on the formating rules for this
-    constant, this might fail. *)
+    constant, this might fail.*)
 val const_id_to_ident : const_descr_ref id -> Ident.t
 
 (** [const_ref_to_name n c] tries to format a constant
 *)
 val type_id_to_ident : Path.t id -> Ident.t
 
+(** [module_id_to_ident m_id] tries to format a module
+    [m_id] as an identifier for target [A.target] using the rules stored
+    in environment [A.env]. 
+*)
+val module_id_to_ident : mod_descr id -> Ident.t
+
 end

File src/coq_backend.ml

View file
  • Ignore whitespace
 
 let lex_skip =
 	function
-		| Ast.Com r -> ml_comment_to_rope r
+    | Ast.Com r -> ml_comment_to_rope r
     | Ast.Ws r -> r
     | Ast.Nl -> r"\n"
 ;;
 ;;
 
 
-let none = Ident.mk_ident [] (Name.add_lskip (Name.from_rope (r"None"))) Ast.Unknown
-;;
-
-let some = Ident.mk_ident [] (Name.add_lskip (Name.from_rope (r"Some"))) Ast.Unknown
-;;
+let none = Ident.mk_ident_strings [] "None";;
+let some = Ident.mk_ident_strings [] "Some";;
 
 let fresh_name_counter = ref 0
 ;;
     kwd (Ulib.Text.to_string @@ Name.to_rope (Name.strip_lskip lskips_t))
 ;;
 
-let rec src_t_to_string =
-  function
-    | Typ_app (p, ts) ->
-      let (name_list, name) = Ident.to_name_list (resolve_ident_path p p.descr) in
-        from_string @@ Ulib.Text.to_string (Name.to_rope name)
-    | Typ_var (_, v) ->
-        id Type_var @@ Ulib.Text.(^^^) (r"") (Tyvar.to_rope v)
-    | Typ_wild skips -> from_string "_"
-    | Typ_len src_nexp -> from_string "(* src_t_to_string len *)"
-    | Typ_fn (src_t, skips, src_t') -> from_string "(* src_t_to_string fn *)"
-    | Typ_tup src_t_lskips_seplist -> from_string "(* src_t_to_string tuple *)"
-    | Typ_paren (skips, src_t, skips') ->
-        from_string "(" ^ src_t_to_string src_t.term ^ from_string ")"
-;;
-
-module CoqBackend (A : sig val avoid : var_avoid_f option;; val env : env end) =
+module CoqBackendAux (A : sig val avoid : var_avoid_f option;; val env : env end) =
   struct
 
     module B = Backend_common.Make (
       end)
     ;;
 
+let rec src_t_to_string =
+  function
+    | Typ_app (p, ts) ->
+      let (name_list, name) = Ident.to_name_list (B.type_id_to_ident p) in
+        from_string @@ Ulib.Text.to_string (Name.to_rope name)
+    | Typ_var (_, v) ->
+        id Type_var @@ Ulib.Text.(^^^) (r"") (Tyvar.to_rope v)
+    | Typ_wild skips -> from_string "_"
+    | Typ_len src_nexp -> from_string "(* src_t_to_string len *)"
+    | Typ_fn (src_t, skips, src_t') -> from_string "(* src_t_to_string fn *)"
+    | Typ_tup src_t_lskips_seplist -> from_string "(* src_t_to_string tuple *)"
+    | Typ_paren (skips, src_t, skips') ->
+        from_string "(" ^ src_t_to_string src_t.term ^ from_string ")"
+;;
 let typ_ident_to_output (p : Path.t id) =     
   Ident.to_output Type_ctor path_sep (B.type_id_to_ident p)
 
       DefaultMap.find k !initial_default_map
     ;;
 
-    let rec def inside_module m =
+    let rec def (callback : def list -> Output.t) (inside_module : bool) (m : def_aux) =
       match m with
       | Type_def (skips, def) ->
           let funcl =	if is_abbreviation def then
                 if in_target targets then
                   let skips' = Util.option_default None skips'_opt in
                   let header =
-                    if snd (Typed_ast_syntax.is_recursive_def ((m, None), Ast.Unknown)) then
+                    if snd (Typed_ast_syntax.is_recursive_def m) then
                       Output.flat [
                         from_string "Program"; ws skips'; from_string "Fixpoint"
                       ]
         end
       | Module (skips, (name, l), mod_binding, skips', skips'', defs, skips''') ->
         let name = lskips_t_to_output name in
-        let body = flat @@ List.map (fun ((d, s), l) ->
-          let skips =
-            match s with
-              | None -> emp
-              | Some s -> ws s
-          in
-          Output.flat [
-            skips; def true d
-          ]) defs
-        in
+        let body = callback defs in
           Output.flat [
             ws skips; from_string "Module "; name; from_string "."; ws skips'; ws skips'';
             body; from_string "\nEnd "; name; from_string "."; ws skips'''
           ]
       | Rename (skips, name, mod_binding, skips', mod_descr) -> from_string "Rename"
       | Open (skips, mod_descr) ->
-          let mod_path = resolve_ident_path mod_descr mod_descr.descr.mod_binding in
+          let mod_path = B.module_id_to_ident mod_descr in
           let mod_name = Ident.get_name mod_path in
           if (mod_name |> Name.strip_lskip |> Name.to_string) = "Vector" then
             Output.flat []
       | Class (skips, skips', name, tyvar, p, skips'', body, skips''') -> from_string "Class"
       | Instance (skips, instantiation, vals, skips', sem_info) -> from_string "Instance"
       | Comment c ->
-      	let ((def_aux, skips_opt), l) = c in
+      	let ((def_aux, skips_opt), l, lenv) = c in
           Output.flat [
-      		  from_string "(* "; def inside_module def_aux; from_string " *)"
+      		  from_string "(* "; def callback inside_module def_aux; from_string " *)"
           ]
       | Ident_rename _ -> from_string "\n(* [?]: removed rename statement. *)"
       | Lemma (skips, lemma_typ, targets, name_skips_opt, skips', e, skips'') ->
           emp
         else
           (from_string "{") ^ (concat_str " " tyvars) ^ (from_string " : Type}")
-    and coq_function_application_to_output id args = B.function_application_to_output exp id args
+    and coq_function_application_to_output l id args = B.function_application_to_output l exp id args
     and exp e =
       let is_user_exp = Typed_ast_syntax.is_trans_exp e in
         match C.exp_to_term e with
                 match C.exp_to_term e0 with
                   | Constant cd -> 
                     (* constant, so use special formatting *)
-                    B.function_application_to_output trans false cd args
+                    B.function_application_to_output (exp_to_locn e) trans false e cd args
                   | _ -> (* no constant, so use standard one *)
                     List.map trans (e0 :: args)
               end in
                 Output.flat [
                   ws skips; from_string "let"; body; ws skips'; from_string "in "; exp e;
                 ]
-          | Constant const -> Output.concat emp (B.function_application_to_output exp false const [])
+          | Constant const -> Output.concat emp (B.function_application_to_output (exp_to_locn e) exp false e const [])
           | Fun (skips, ps, skips', e) ->
               let ps = fun_pattern_list ps in
                 block_hov (Typed_ast_syntax.is_trans_exp e) 2 (
                match C.exp_to_term c with
                  | Constant cd -> 
                    (* constant, so use special formatting *)
-                   B.function_application_to_output trans true cd [l;r]
+                   B.function_application_to_output (exp_to_locn e) trans true e cd [l;r]
                  | _ -> (* no constant, so use standard one *)
                    List.map trans [l;c;r]
             end in
               from_string "(" ^ body ^ from_string ") % type"
         | Typ_app (p, ts) ->
           let args = concat_str " " @@ List.map abbreviation_typ ts in
-          let (name_list, name) = Ident.to_name_list (resolve_ident_path p p.descr) in
+          let (name_list, name) = Ident.to_name_list (B.type_id_to_ident p) in
           let arg_sep = if List.length ts > 1 then from_string " " else emp in
             Output.flat [
               kwd @@ Ulib.Text.to_string (Name.to_rope name); arg_sep; args
     	match Seplist.hd def with
       	| (n, tyvars, _, (Te_record (skips, skips', fields, skips'') as r),_) ->
             let (n', _) = n in
- 	                let name = Name.to_output Type_ctor n' in
-      			let body = flat @@ Seplist.to_sep_list_last (Seplist.Forbid (fun x -> emp)) field (sep @@ from_string ";") fields in
-      			let tyvars' = type_def_type_variables tyvars in
+            let name = Name.to_output Type_ctor n' in
+            let body = flat @@ Seplist.to_sep_list_last (Seplist.Forbid (fun x -> emp)) field (sep @@ from_string ";") fields in
+      	    let tyvars' = type_def_type_variables tyvars in
             let tyvar_sep = if List.length tyvars = 0 then emp else from_string " " in
             let boolean_equality = generate_coq_record_equality tyvars n fields in
       			  Output.flat [
           Name.to_output Term_field (B.const_ref_to_name n f_ref); 
           from_string ":"; ws skips; field_typ t
       ]
-    and defs inside_module (ds : def list) =
-      	List.fold_right (fun ((d, s), l) y ->
-          match s with
-            | None   -> def inside_module d ^ y
-            | Some s -> def inside_module d ^ ws s ^ y
-      	) ds emp
     and generate_default_value_texp (t: texp) =
       match t with
         | Te_opaque -> from_string "DAEMON"
         let mapped = List.map generate_default_value ts in
           concat_str "\n" mapped
       ;;
+end
+;;
+
+
+
+module CoqBackend (A : sig val avoid : var_avoid_f option;; val env : env end) =
+  struct
+
+    let rec defs inside_module (ds : def list) =
+      	List.fold_right (fun (((d, s), l, lenv):def) y ->
+          let module C = CoqBackendAux (
+             struct
+                let avoid = A.avoid;;
+                let env = {A.env with local_env = lenv}
+             end) in
+          let callback = defs true in
+          match s with
+            | None   -> C.def callback inside_module d ^ y
+            | Some s -> C.def callback inside_module d ^ ws s ^ y
+      	) ds emp
 
     let coq_defs ((ds : def list), end_lex_skips) =
     	to_rope (r"\"") lex_skip need_space @@ defs false ds ^ ws end_lex_skips
     ;;
+
 end
-;;

File src/def_trans.ml

View file
  • Ignore whitespace
               | None -> ( 
                   let (env',def') = 
                     match def with
-                      | ((Module(sk1,(n,l'),mod_bind,sk2,sk3,ds,sk4),s),l) ->
+                      | ((Module(sk1,(n,l'),mod_bind,sk2,sk3,ds,sk4),s),l,lenv) ->
                           let (env',ds') = 
                             process_defs (mod_name::path) trans (Name.strip_lskip n) env ds 
                           in
-                            (env',((Module(sk1,(n,l'),mod_bind,sk2,sk3,ds',sk4),s),l))
+                            (env',((Module(sk1,(n,l'),mod_bind,sk2,sk3,ds',sk4),s),l,lenv))
                       | _ -> (env,def)
                   in
                   let (env'', defs') = p env' defs in
 
 module C = Exps_in_context (struct let avoid = None let env_opt = Some E.env end)
 
-let simple_def d = [((d,None),Ast.Unknown)]
+(* let simple_def d = [((d,None),Ast.Unknown)] *)
 
-let remove_vals _ env (((d,s),l) as def) =
+let comment_def ((((d, s), l, lenv):def) as def) : def =
+  ((Comment (def), s), Ast.Trans("comment_def", Some l), lenv)
+
+let remove_vals _ env (((d,_),_,_) as def) =
   match d with
     | Val_spec _ ->
-        Some((env, simple_def (Comment(def))))
+        Some (env, [comment_def def])
     | _ -> None
 
-let remove_indrelns _ env (((d,s),l) as def) =
+let remove_indrelns _ env (((d,_),_,_) as def) =
   match d with
     | Indreln _ ->
-        Some((env, simple_def (Comment(def))))
+        Some (env, [comment_def def])
     | _ -> None
 
-let remove_opens _ env (((d,s),l) as def) =
+let remove_opens _ env (((d,_),_,_) as def) =
   match d with
     | Open _ ->
-        Some((env, simple_def (Comment(def))))
+        Some (env, [comment_def def])
     | _ -> None
 
-let remove_classes _ env (((d,s),l) as def) =
+let remove_classes _ env (((d,_),_,_) as def) =
   match d with
     | Class _ ->
-        Some((env, simple_def (Comment(def))))
+        Some(env, [comment_def def])
     | _ -> None
 
-let remove_indrelns_true_lhs _ env ((d,s),l) =
+let remove_indrelns_true_lhs _ env ((d,s),l,lenv) =
   let l_unk = Ast.Trans ("remove_indrelns_true_lhs", Some l) in
   match d with
     | Indreln (s', targ, sl) ->
         (match Seplist.map_changed remove_true sl with
              None -> None
            | Some sl' -> 
-             let def = (((Indreln (s', targ, sl'), s), l_unk):def) in 
+             let def = (((Indreln (s', targ, sl'), s), l_unk, lenv):def) in 
              Some(env, [def]))
     | _ -> None
 
         else
           Some (None,C.t_to_src_t (exp_to_typ e))
              
-let type_annotate_definitions _ env ((d,s),l) =
+let type_annotate_definitions _ env ((d,s),l,lenv) =
   match d with
     | Val_def(Let_def(sk1,topt,(p, name_map, src_t_opt, sk2, e)),tnvs,class_constraints) -> begin
         match generate_srt_t_opt src_t_opt e with
           | None -> None
           | Some t -> Some (env,
-               [((Val_def(Let_def(sk1, topt,(p, name_map, Some t, sk2, e)), tnvs, class_constraints), s), l)])
+               [((Val_def(Let_def(sk1, topt,(p, name_map, Some t, sk2, e)), tnvs, class_constraints), s), l, lenv)])
       end
     (* TODO: Handle Fun_def *)
     | Val_def(Fun_def(sk1,sk2,topt,funs),tnvs,class_constraints) -> begin
         match funs'_opt with 
           | None -> None
           | Some funs' -> Some (env,
-               [((Val_def(Fun_def(sk1,sk2,topt,funs'), tnvs, class_constraints), s), l)])
+               [((Val_def(Fun_def(sk1,sk2,topt,funs'), tnvs, class_constraints), s), l, lenv)])
       end
     | _ -> None
 
 
 let dict_type_name cn = (Name.lskip_rename (fun x -> Ulib.Text.(^^^) x (r"_class")) cn)
 
-let class_to_module mod_path env ((d,s),l) =
+let class_to_module mod_path env ((d,s),l,lenv) =
 (*  let l_unk = Ast.Trans("class_to_module", Some l) in *)
     match d with
       | Class(sk1,sk2,(n,l),tnvar,class_path,sk3,specs,sk4) ->
             Type_def (Ast.combine_lex_skips sk1 sk2, 
                       Seplist.from_list_default None [((dict_type_name n, l), [tnvar], class_path, Te_record(None, sk3, fields, sk4), None)])
           in
-            Some((env, (simple_def rec_def)))
+            Some (env, [((rec_def, s), l, lenv)])
       | _ -> None
 
 
-let instance_to_module (global_env : env) mod_path (env : env) ((d,s),l) =
+let instance_to_module (global_env : env) mod_path (env : env) ((d,s),l,lenv) =
   let l_unk n = Ast.Trans("instance_to_module" ^ string_of_int n , Some l) in
   match d with
       | Instance(sk1, (prefix, sk2, id, t, sk3), vdefs, sk4, sem_info) ->
           let m = 
             Module(sk1, (Name.add_lskip sem_info.inst_name, l_unk 9), 
                    Path.mk_path mod_path sem_info.inst_name, sk2, None, 
-                   List.map (fun d -> ((Val_def(d,tnvars_set,sem_info.inst_constraints),None), l_unk 10)) 
+                   List.map (fun d -> ((Val_def(d,tnvars_set,sem_info.inst_constraints),None), l_unk 10, lenv)) 
                             (vdefs @ [dict]), 
                    sk4)
           in
-            Some((env,[((m,s),l)]))
+            Some((env,[((m,s),l,lenv)]))
       | _ ->
           None
 
-let class_constraint_to_parameter : def_macro = fun mod_path env ((d,s),l) ->
+let class_constraint_to_parameter : def_macro = fun mod_path env ((d,s),l,lenv) ->
   let l_unk = Ast.Trans("class_constraint_to_parameter", Some l) in
   (* TODO : avoid shouldn't be None *)
     match d with
       | _ -> None
 
 
-let nvar_to_parameter : def_macro = fun mod_path env ((d,s),l) ->
+let nvar_to_parameter : def_macro = fun mod_path env ((d,s),l,_) ->
   let l_unk = Ast.Trans("nvar_to_parameter", Some l) in
     match d with
       | Val_def(lb, tnvs, class_constraints) ->
     | (Target.Target_ocaml, Ast.Lemma_lemma _) -> false
     | (_, _) -> true
 
-let prune_target_bindings target defs =
+let prune_target_bindings target (defs : def list) : def list =
 
   (* given a list constant name and a list of definition, rem_dups removes all
    * duplicate definitions (i.e. with the same name) from the list *)
   let rec rem_dups name = function 
     | [] -> []
-    | ((def,s),l)::defs -> 
+    | ((def,s),l, lenv)::defs -> 
         (match def with 
       | (Val_def _ | Indreln _) -> 
           if (Name.compare name (get_name def l) = 0) then
             rem_dups name defs
           else 
-            ((def,s),l) :: rem_dups name defs
-      | d -> ((d,s),l) :: rem_dups name defs
+            ((def,s),l,lenv) :: rem_dups name defs
+      | d -> ((d,s),l,lenv) :: rem_dups name defs
     )
   in
 
   let rec def_walker (target : Target.non_ident_target) acc =  function
     | [] -> List.rev acc
 
-    | ((def,s),l)::defs -> begin
+    | ((def,s),l,lenv)::defs -> begin
       match def with
         | (Val_def(Let_def(_,topt,_),_,_) |
           Val_def(Fun_def(_,_,topt,_),_,_) |
               let name = get_name d l in
               let acc' = rem_dups name acc in  
               let defs' = rem_dups name defs in
-            def_walker target (((def,s),l) :: acc') defs' 
+            def_walker target (((def,s),l,lenv) :: acc') defs' 
           else
             def_walker target acc defs
       
        | Lemma(_,lty,targets,_,_,_,_) as d ->
          let targ_OK = Typed_ast.in_targets_opt (Target_no_ident target) targets in
          if (target_supports_lemma_type target lty && targ_OK) then
-            def_walker target (((d,s),l) :: acc) defs
+            def_walker target (((d,s),l,lenv) :: acc) defs
          else
             def_walker target acc defs
-       | d -> def_walker target (((d,s),l) :: acc) defs
+       | d -> def_walker target (((d,s),l,lenv) :: acc) defs
      end
 
   in def_walker target [] defs

File src/ident.ml

View file
  • Ignore whitespace
   fprintf ppf "%a" 
     (Pp.lst "." error_pp_help) (ns @ [n])
 
-
-let mk_ident_names m n = (None, m, n)
-
-let mk_ident m n l : t = 
+let mk_ident_ast m n l : t = 
   let ms = List.map (fun (n,sk) -> n) m in
   let prelim_id = (None, m, (n,None)) in
     List.iter (fun (_, sk) ->
             (ms' @ [n]);
           (Name.get_lskip m', List.map Name.strip_lskip (m'::ms'), Name.strip_lskip n)
 
-let mk_ident_names l i =
-  mk_ident (List.map (fun r -> (Name.add_lskip r, None)) l)
-    (Name.add_lskip i)
-    (Ast.Trans ("mk_ident_names", None))
+let mk_ident sk m n = ((sk, m, n) : t)
 
 let mk_ident_strings l i =
-  mk_ident_names (List.map (fun n -> Name.from_string n) l) (Name.from_string i) 
+  mk_ident None (List.map (fun n -> Name.from_string n) l) (Name.from_string i) 
 
 let from_id (Ast.Id(m,xl,l)) : t =
-  mk_ident 
+  mk_ident_ast
     (List.map (fun (xl,l) -> (Name.from_x xl, l)) m)
     (Name.from_x xl)
     l

File src/ident.mli

View file
  • Ignore whitespace
 (** Return the last name in the ident, e.g., M.Y.x gives x *)
 val get_name : t -> Name.lskips_t
 
-(** [mk_ident nsl ns l] generates a new identifiers giving full control. Whitespace is prohibited though and
-    only parenthesis might be used in the [Name.lskips_t]. Otherwise, this operation my fails and uses
-    the location [l] for the error message. *)
-val mk_ident : (Name.lskips_t * Ast.lex_skips) list -> Name.lskips_t -> Ast.l -> t
+(** [mk_ident sk ms n] creates an identifier [n] with module prefix [ms] and leading whitespace [sk]. *)
+val mk_ident : Ast.lex_skips -> Name.t list -> Name.t -> t
 
-(** Since [mk_ident] does not allow whitespace and parenthesis are often not needed, 
-    [mk_ident_names] provides a simpler interface that uses names. Since it cannot fail, the location is
-    not needed. *)
-val mk_ident_names : Name.t list -> Name.t -> t
+(** [mk_ident_ast nsl ns l] generates a new identifiers during type-checking. Whitespace is prohibited in all [Name.lskips_t] except the very first one
+    and all [Ast.lex_skips] has to be empty. Otherwise, this operation my fails and uses the location [l] for the error message. *)
+val mk_ident_ast : (Name.lskips_t * Ast.lex_skips) list -> Name.lskips_t -> Ast.l -> t
 
-(** [mk_ident_strings] is a version of [mk_ident_names] that uses strings as input. *)
+(** [mk_ident_strings] is a version of [mk_ident] that uses strings as input and uses empty whitespace. *)
 val mk_ident_strings : string list -> string -> t
 
-
 val to_output : Output.id_annot -> Output.t -> t -> Output.t
 val to_output_infix : (Output.id_annot -> Ulib.Text.t -> Output.t) -> Output.id_annot -> Output.t -> t -> Output.t
 val get_first_lskip: t -> Ast.lex_skips

File src/initial_env.mli

View file
  • Ignore whitespace
 (**************************************************************************)
 
 open Types
-type t = 
-    Typed_ast.env * (Target.target * Ulib.Text.t list) list
+type t = Typed_ast.env * (Target.target * Ulib.Text.t list) list
 val add_to_init : Target.non_ident_target -> string -> t -> t
 
 module Initial_libs(P : sig val path : string end) : sig

File src/macro_expander.ml

View file
  • Ignore whitespace
                       List.map (expand_exp (r,typ_r,src_typ_r,pat_r)) es))
                   c)
     | Module(sk1, nl, mod_path, sk2, sk3, ds, sk4) ->
-        Module(sk1, nl, mod_path, sk2, sk3, List.map (fun ((d,s),l) -> ((expand_def d,s),l)) ds, sk4)
+        Module(sk1, nl, mod_path, sk2, sk3, List.map (fun ((d,s),l,lenv) -> ((expand_def d,s),l,lenv)) ds, sk4)
     | Instance(sk1,is,vdefs,sk2,sem_info) ->
         Instance(sk1, is, List.map expand_val_def vdefs, sk2, sem_info)
     | def -> def
   in
     match defs with
       | [] -> []
-      | ((def,s),l)::defs ->
-          ((expand_def def,s),l)::expand_defs defs (r,typ_r,src_typ_r,pat_r)
+      | ((def,s),l,lenv)::defs ->
+          ((expand_def def,s),l,lenv)::expand_defs defs (r,typ_r,src_typ_r,pat_r)
 end

File src/name.ml

View file
  • Ignore whitespace
 
 let fresh s ok = from_rope (fresh_start None s ok)
 
-let rec fresh_list i s ok =
+let rec fresh_num_list i s ok =
   if i = 0 then
     []
   else begin
     let new_name = from_rope (fresh_start (Some(i)) s ok) in
     let new_ok n = ok n && (n <> new_name) in
-    new_name :: fresh_list (i - 1) s new_ok
+    new_name :: fresh_num_list (i - 1) s new_ok
   end
 
 
+let rec fresh_list_aux (acc : t list) (ok : t -> bool) = function
+  | []      -> List.rev acc
+  | n :: ns -> begin
+      let n' = fresh (to_rope n) ok in
+      let ok' n =  ok n && (n <> n') in
+      fresh_list_aux (n'::acc) ok' ns
+    end 
 
+let fresh_list ok ns = fresh_list_aux [] ok ns
 
 let rename f r = from_rope (f (to_rope r))
 
   to_output a (s, (r"\"" ^^ x ^^ r"\""))
 
 let to_rope_tex a n = 
-  Output.to_rope_ident a (to_rope n)
+  Output.to_rope_tex (Output.id a (to_rope n))
 
 let add_pre_lskip lskip (s,x) = 
   (Ast.combine_lex_skips lskip s,x)

File src/name.mli

View file
  • Ignore whitespace
     Then counting up from 0 starts, till [OK] is satisfied. *)
 val fresh : Ulib.Text.t -> (t -> bool) -> t
 
-(** [fresh_list i n OK] generates a list of [i] fresh names. Internally,
+(** [fresh_num_list i n OK] generates a list of [i] fresh names. If no conflicts occur
+    it returns a list of the form [[ni, n(i-1), ..., n1]]. Internally,
     [fresh n OK] is used [n] times. However, [OK] is updated to ensure, that
-    the elemenst of the resulting list are also distinct from each other. *)
-val fresh_list : int -> Ulib.Text.t -> (t -> bool) -> t list
+    the elemenst of the resulting list not only satisfy [OK], but are also distinct from each other. *)
+val fresh_num_list : int -> Ulib.Text.t -> (t -> bool) -> t list
+
+(** [fresh_list OK ns] builds variants of the names in list [ns] such that all elements of 
+    the resulting list [ns'] satisfy [OK] and are distinct to each other.*)
+val fresh_list : (t -> bool) -> t list -> t list
 
 (** [rename r_fun n] renames [n] using the function [r_fun]. It looks at the 
   text representation [n_text] of [n] and returns then the name corresponding to

File src/output.ml

View file
  • Ignore whitespace
   | Class_name
   | Target
 
-
 type block_type =
     Block_type_hbox
   | Block_type_vbox of int
   | Block_type_hvbox d  -> Format.pp_open_hvbox ff d
   | Block_type_hovbox d -> Format.pp_open_hovbox ff d
 
-
 type t = 
   | Empty                          (* Empty output *)
   | Kwd of string                  (* Keyword *)
   | Num' of int
 
 let emp = Empty
-
 let kwd t = Kwd(t)
-
 let id a t = Ident(a,t)
-
 let num t = Num(t)
 
 let ws = function
            (List.rev ts))
 
 let str s = Str(s)
-
 let err s = Err(s)
-
 let meta s = Meta(s)
 
 let texspace = Texspace
 (* Debug pp *)
 (* ******** *)
 
-
 let pp_raw_id_annot = function
   | Term_const         -> r"Term_const"       
   | Term_ctor          -> r"Term_ctor"        
   | Internalspace -> r"Internalspace"
 
 
-
-
 (* turns a single, unstructered Output.t into a string *)
 let to_rope_single quote_char lex_skips_to_rope preserve_ws t : Ulib.Text.t = 
   match t with
 
 
 
-(* ************* *)
-(* LaTeX backend *)
-(* ************* *)
+
+
+(******************************************************************************)
+(* LaTeX backend                                                              *)
+(******************************************************************************)
 
 let tex_command_prefix = r"LEM"  (* for LaTeX commands in generated .tex and -inc.tex files *)
 let tex_label_prefix   = r"lem:" (* for LaTeX labels in generated .tex and -inc.tex files *)
 let tex_sty_prefix     = r"lem"  (* for LaTeX commands in the lem.sty file *)
 
 (* escaping of Lem source names to use in LaTeX command names
- (probably it needs to be more aggressive)
- (and it isn't injective, so we should do some global check or rename too...) *)
+   (probably it needs to be more aggressive)
+   (and it isn't injective, so we should do some global check or rename too...) *)
 let tex_command_escape rr = 
   Ulib.Text.concat
     Ulib.Text.empty
 
 let debug = false
 
-let to_rope_ident a rr =
+let to_rope_tex_ident a rr =
   let (r1,r2) = split_suffix_rope rr in
   tex_id_wrap a ^^ r"{" ^^ tex_escape r1 ^^ r"}" ^^ r2
 
-let quote_char = r"\""
-
 let rec to_rope_tex_single t = 
   match t with
   | Empty -> r""
   | Kwd(s) ->  Ulib.Text.of_latin1 s
-  | Ident(a,r) -> to_rope_ident a r
+  | Ident(a,r) -> to_rope_tex_ident a r
   | Num(i) ->  Ulib.Text.of_latin1 (string_of_int i)
   | Inter(Ast.Com(rr)) -> r"\\tsholcomm{" ^^ tex_escape (ml_comment_to_rope rr)  ^^ r"}" 
   | Inter(Ast.Ws(rr)) -> rr
   | Inter(Ast.Nl) -> raise (Failure "Nl in to_rope_tex")
-  | Str(s) ->  quote_string quote_char s
+  | Str(s) ->  quote_string (r"\"") s
   | Err(s) -> raise (Backend(s))
   | Meta(s) -> Ulib.Text.of_latin1 s
   | Texspace -> r"\\ "   
   | Cons(t1,t2) -> raise (Failure "Cons in to_rope_tex") 
   | Block _ -> raise (Failure "Block in to_rope_tex") 
 
-
-let make_indent r = 
+(** [make_indent r] returns a text consisting only of spaces of the same length as [r] *)
+let make_indent (r : Ulib.Text.t) : Ulib.Text.t = 
   let n = Ulib.Text.length r in
   let single_indent = "\\ " in
   let rec n_of x n = if n=0 then [] else x::n_of x (n-1) in
   let rec strip_initial_texspace ts = match ts with
   | [] -> [] 
   | Texspace :: ts' -> strip_initial_texspace ts'
-  | _ :: ts' -> ts in
-  List.rev (strip_initial_texspace (List.rev (strip_initial_texspace ts))) 
+  | _ :: ts' -> ts in List.rev (strip_initial_texspace (List.rev (strip_initial_texspace ts))) 
     
-
 (* returns None if all whitespace or texspace, otherwise Some of the indented rope *)
-let to_rope_option_line : t list -> Ulib.Text.t option 
+let to_rope_tex_option_line : t list -> Ulib.Text.t option 
     = function ts -> 
       let rec f indent_acc ts = 
         match ts with
   let rec strip_initial tss = match tss with
   | [] -> []
   | None::tss' -> strip_initial tss'
-  | _ :: _ -> tss in
-  let dummy_space tso = match tso with 
-  | None -> r"\\ "  (* to workaround latex tabbing sensitivity *)
-  | Some r -> r in
-  List.map dummy_space (List.rev (strip_initial (List.rev (strip_initial tss)))) 
+  | _ :: _ -> tss in begin
+    let dummy_space tso = match tso with 
+      | None -> r"\\ "  (* to workaround latex tabbing sensitivity *)
+      | Some r -> r in 
+    List.map dummy_space (List.rev (strip_initial (List.rev (strip_initial tss)))) 
+  end
 
-let rec to_rope_lines strip_blanks tss = 
+let rec to_rope_tex_lines strip_blanks tss = 
   let rs = if strip_blanks then 
     strip_initial_and_final_blank_lines 
-      (List.map to_rope_option_line tss)
+      (List.map to_rope_tex_option_line tss)
   else
     List.map
       (function | None -> r"" | Some r -> r) 
-      (List.map to_rope_option_line tss) in
+      (List.map to_rope_tex_option_line tss) in
 
   let rec f rs = 
     match rs with
   | _ -> Some (f rs) 
 
 
-let to_rope_option_tex term need_space strip_blanks t = 
-
+let to_rope_option_tex t = 
   if debug then Printf.printf "\n\n\nto_rope_tex input:\n%s" (Ulib.Text.to_string (pp_raw_t t));
 
   let lines = line_break (flatten_to_list t) in
-  
-  let ro = to_rope_lines strip_blanks lines in
+  let ro = to_rope_tex_lines true lines in
   
   (if debug then Printf.printf "\n\nto_rope_tex output:\n%s" (Ulib.Text.to_string (match ro with None -> r"None" | Some rr -> r"Some(" ^^ rr ^^ r")")));
   
   ro
 
 
+let to_rope_tex t = 
+  match to_rope_option_tex t with
+    | None -> r""
+    | Some rr -> rr
+

File src/output.mli

View file
  • Ignore whitespace
 (** a single space *)
 val space : t
 
+(** ??? Unsure what it is. Some kind of tex specific space, similar to space, but
+    treated slightly differently by the Latex backend. It seems to be for example removed
+    at beginnings and ends of lines and multiple ones are collapsed into a single space. *)
+val texspace :  t
+
+
 (** An identifier *)
 val id : id_annot -> Ulib.Text.t -> t
 
 
 (** {2 Output to Rope} *)
 
+(** [to_rope quote_char lex_skips_to_rope need_space t] formats the output [t] as an unicode text.
+The [quote_char] argument is used around strings. The function [lex_skips_to_rope] is used to format
+whitespace. Finally the function [need_space] is used to determine, whether an extra space is needed between
+simplified outputs. *)
 val to_rope : Ulib.Text.t -> (Ast.lex_skip -> Ulib.Text.t) -> (t' -> t' -> bool) -> t -> Ulib.Text.t
-val to_rope_option_tex : (Ast.lex_skip -> Ulib.Text.t) -> (t' -> t' -> bool) -> bool -> t -> Ulib.Text.t option
-val to_rope_ident : id_annot ->  Ulib.Text.t -> Ulib.Text.t
 
-val tex_escape : Ulib.Text.t -> Ulib.Text.t
+(** [ml_comment_to_rope com] formats an ML-comment as a text by putting [(*] and [*)] around it. *)
+val ml_comment_to_rope : Ast.ml_comment -> Ulib.Text.t
+
+
+(** {2 Latex Output} *)
 
+(** [to_rope_tex t] corresponds to [to_rope] for the Latex backend. Since it is used for only one backend,
+    the backend parameters of [to_rope] can be hard-coded.  *)
+val to_rope_tex : t -> Ulib.Text.t 
+
+(** [to_rope_option_tex t] is similar to [to_rope_tex t]. However, it checks whether the
+    result is an empty text and returns [None] is in this case. *)
+val to_rope_option_tex : t -> Ulib.Text.t option
+
+val tex_escape : Ulib.Text.t -> Ulib.Text.t
 val tex_command_escape : Ulib.Text.t -> Ulib.Text.t
 val tex_command_label  : Ulib.Text.t -> Ulib.Text.t
 val tex_command_name  : Ulib.Text.t -> Ulib.Text.t
 
-val ml_comment_to_rope : Ast.ml_comment -> Ulib.Text.t
-
-
-(** {2 ???} *)
-val texspace :  t

File src/path.ml

View file
  • Ignore whitespace
 
 let (^) = Ulib.Text.(^^^)
 
-let to_ident p =  match to_name_list p with 
-     (vs,v) -> 
-        Ident.mk_ident 
-          (List.map (fun v -> (Name.add_lskip v, None)) vs) 
-          (Name.add_lskip v)
-          Ast.Unknown
+let to_ident sk p =  match to_name_list p with 
+     (vs,v) -> Ident.mk_ident sk vs v
 
 let numpath = Path_num
 

File src/path.mli

View file
  • Ignore whitespace
 val unitpath : t
 val get_name : t -> Name.t
 val check_prefix : Name.t -> t -> bool
-val to_ident : t -> Ident.t
+val to_ident : Ast.lex_skips -> t -> Ident.t
 val to_name : t -> Name.t
 val to_name_list : t -> Name.t list * Name.t
 (*

File src/patterns.ml

View file
  • Ignore whitespace
          match dest_var_pat p with Some n -> n
            | None -> Name.from_rope (r "_")
 
-let def_to_pat_matrix_list (((d, _), l) : def) : (Name.t * (bool * pat_matrix) * Ast.l) list = match  d with 
+let def_to_pat_matrix_list (((d, _), l,_) : def) : (Name.t * (bool * pat_matrix) * Ast.l) list = match  d with 
   |  Val_def ((Fun_def (_, _, _, sl)), _,_) -> begin 
        let (_, _, sll) = funcl_aux_seplist_group sl in
        let to_m (n, (sl:funcl_aux lskips_seplist)) = (n, (false, funcl_aux_list_to_pat_matrix (Seplist.to_list sl)), l) in
     stored under module path [mp] and name [n]. *)
 let make_id (mp: Name.t list option) (n : Name.t) inst (c:const_descr_ref) : (const_descr_ref id) =
   let loc = Ast.Trans ("constr_matrix_compile_make_id", None) in
-  let id_p = match mp with None -> Id_none None | Some mp -> Id_some (Ident.mk_ident_names mp n) in
+  let id_p = match mp with None -> Id_none None | Some mp -> Id_some (Ident.mk_ident None mp n) in
   { id_path = id_p;
     id_locn = loc;
     descr = c;
    end
 
     
-let compile_def t mca env_global (_:Name.t list) env_local (((d, s), l) as org_d : def) =  
+let compile_def t mca env_global (_:Name.t list) env_local (((d, s), l, lenv) as org_d : def) =  
  let env = env_global in
  let cf_opt e = compile_match_exp t mca env e in
  let cf e = Util.option_default e (cf_opt e) in
  let constr topt tnvs class_constraints s1 s2 sl =       
-       Util.option_map (fun d -> (env_local, [(((Val_def (d, tnvs,class_constraints),s), l):def)]))
+       Util.option_map (fun d -> (env_local, [(((Val_def (d, tnvs,class_constraints),s), l, lenv):def)]))
          (compile_faux_seplist l env cf s1 s2 t topt org_d sl) in
- if mca.def_OK env ((d, s), l) then None else
+ if mca.def_OK env org_d then None else
  match d with
   |  Val_def (Fun_def (s1, s2_opt, topt, sl), tnvs,class_constraints) -> begin 
        if not (in_targets_opt t topt) then None else 
    let rec f p1 = e1 
        and f p2 = e2 ... *)
   
-let remove_toplevel_match targ mca env_global _ env_local (((d, s), l)) =
+let remove_toplevel_match targ mca env_global _ env_local (((d, s), l, lenv)) =
   let l_unk = Ast.Trans ("remove_toplevel_match", Some l) in
   let env = env_global in
   let aux sk1 sk2_opt topt sl tnvs class_constraints = begin
           | _ -> None) in
     match (Util.map_changed group_apply groupL) with None -> None | Some sll' ->
       let sl' = Seplist.flatten space sll' in
-      let new_d = ((Val_def ((Fun_def (sk1, sk2_opt, topt, sl')), tnvs, class_constraints), s), l) in
+      let new_d = ((Val_def ((Fun_def (sk1, sk2_opt, topt, sl')), tnvs, class_constraints), s), l, lenv) in
       if mca.def_OK env new_d then Some (env_local, [new_d]) else None
   end in
   match d with 

File src/rename_top_level.ml

View file
  • Ignore whitespace
 open Target
 open Util
 
-let flatten_modules_macro path env ((d,s),l) =
+let flatten_modules_macro path env ((d,s),l,lenv) =
   let l_unk = Ast.Trans("flatten_modules", Some l) in
     match d with
       | Module(sk1,n,mod_path,sk2,sk3,ds,sk4) ->
-          let mod_shell = ((Module(sk1,n,mod_path,sk2,sk3,[],sk4),s),l) in
-          let com = ((Comment(mod_shell),None),l_unk) in
+          let mod_shell = ((Module(sk1,n,mod_path,sk2,sk3,[],sk4),s),l,lenv) in
+          let com = ((Comment(mod_shell),None),l_unk,lenv) in
             Some((env,com::ds))
       | _ -> None
 
 
 let compute_target_rename_constant_fun (targ : Target.non_ident_target) (nk : name_kind) (n : Name.t) : Name.t option =
   match targ with 
-    | Target_ocaml -> compute_ocaml_rename_constant_fun nk n
+    | Target_ocaml -> compute_ocaml_rename_constant_fun nk n 
     | _ -> None
 
 let get_fresh_name consts consts' n = 

File src/reporting.ml

View file
  • Ignore whitespace
 
 let warn_source_to_locn = function
     Warn_source_exp e -> Typed_ast.exp_to_locn e
-  | Warn_source_def (_, l) -> l
+  | Warn_source_def (_, l, _) -> l
   | Warn_source_unkown -> Ast.Unknown
   
 type warning = 
 (* Debuging                                                                   *)
 (******************************************************************************)
 
-let debug_flag = ref true
-
-let print_debug s =
-  if (not !debug_flag) then () else
-  (Format.eprintf "DEBUG: %s\n\n" s;
-   Format.pp_print_flush Format.err_formatter ())
-
 let print_debug_data f s xs =
   let xs_s = List.map (fun x -> Ulib.Text.to_string (f x)) xs in
   print_debug (s ^ "\n" ^ (String.concat "\n" xs_s))

File src/reporting.mli

View file
  • Ignore whitespace
 
 (** Command line options for warnings *)
 val warn_opts : (string * Arg.spec * string) list
-
+  
 (** Turn off pattern compilation warnings, used by main *)
 val ignore_pat_compile_warnings : unit -> unit
 
 
 (** {2 Debuging } *)
 
-(** Should debug be printed *)
-val debug_flag : bool ref
-
-val print_debug : string -> unit
 val print_debug_exp : Typed_ast.env -> string -> Typed_ast.exp list -> unit
 val print_debug_def : Typed_ast.env -> string -> Typed_ast.def list -> unit
 val print_debug_pat : Typed_ast.env -> string -> Typed_ast.pat list -> unit

File src/reporting_basic.ml

View file
  • Ignore whitespace
   (print_err_internal true verb_pos false pos_l m1 m2; exit 1)
 
 
+(******************************************************************************)
+(* Debuging                                                                   *)
+(******************************************************************************)
+
+let debug_flag = ref true
+
+let print_debug s =
+  if (not !debug_flag) then () else
+  (Format.eprintf "DEBUG: %s\n\n" s;
+   Format.pp_print_flush Format.err_formatter ())
 

File src/reporting_basic.mli

View file
  • Ignore whitespace
 *)
 val print_err : bool -> bool -> bool -> Ast.l -> string -> string -> unit
 
+(** {2 Debuging } *)
+
+(** Should debug be printed *)
+val debug_flag : bool ref
+
+(** [print_debug s] prints the string [s] with some debug prefix to the standard error output. *)
+val print_debug : string -> unit 
+
 (** {2 Errors } *)
 
 (** In contrast to warnings, errors always kill the current run of Lem. They can't be recovered from. 

File src/syntactic_tests.ml

View file
  • Ignore whitespace
     cases are for type definitions and modules, which may also define a
     type).
  *)
-let rec check_decidable_equality_def' env (((d, _), l) : def) (in_module_scope : bool) : unit =
+let rec check_decidable_equality_def' env (((d, _), l, _) : def) (in_module_scope : bool) : unit =
   match d with
     | Type_def (_, seplist) ->
         let texps = Seplist.to_list seplist in
     | _ -> InductiveMap.empty
 ;;
 
-let gather_inductive_types (((d, _), _) : def) : src_t list InductiveMap.t =
+let gather_inductive_types (((d, _), _, _) : def) : src_t list InductiveMap.t =
   match d with
     | Type_def (_, seplist) ->
       let texps = Seplist.to_list seplist in
 
 let check_positivity_condition_def (d : def) : unit =
   let inductive_types = gather_inductive_types d in
-  let ((d, _), _) = d in
+  let ((d, _), _, _) = d in
     match d with
       | Type_def (_, seplist) ->
           let texps = Seplist.to_list seplist in

File src/target_binding.ml

View file
  • Ignore whitespace
 (*  IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.                         *)
 (**************************************************************************)
 
-(* Traversing expressions to resolve any target problems that will arise from
- * its binding and module structure and namespaces being different from Lem's *)
-
 open Typed_ast
+open Typed_ast_syntax
 
-module M = Macro_expander.Expander(struct let avoid = None let env_opt = None end)
-module C = Exps_in_context(struct let avoid = None let env_opt = None end)
-module P = Precedence
 
-(* TODO: This needs to be much more complex to be really right *)
-let id_fix_binding (target : Target.non_ident_target) id =
-  match id.id_path with
-    | Id_none _ -> id
-    | Id_some p -> 
-        { id with id_path = Id_some (Ident.strip_path (Target.non_ident_target_to_mname target) p) }
+(* Given some entity of the form [m1. ... . mn . name] the function 
+   [minimize_module_prefix eq_fun env [m1, ... , mn]] tries minimize the module prefix
+   needed to describe [name]. It is first checked, whether [name] means the same as the full
+   prefixed version in [env]. If this is not the case, the function tries to chop of 
+   module names at the beginning, as long as the meaning in [env] is preserved. In order to check
+   whether it "means" the same, the function [eq_fun] is applied to the local environments reachable from [env]
+   with the different module prefixes.
 
-let rec fix_src_t (target : Target.non_ident_target) t =
-  match t.term with
-    | Typ_wild _ | Typ_var _ -> t
-    | Typ_fn(t1,sk,t2) -> 
-        { t with term = Typ_fn(fix_src_t target t1, sk, fix_src_t target t2) }
-    | Typ_tup(ts) -> 
-        { t with term = Typ_tup(Seplist.map (fix_src_t target) ts) }
-    | Typ_app(id,ts) ->
-        { t with term = 
-            Typ_app(id_fix_binding target id, List.map (fix_src_t target) ts) }
-    | Typ_len(n) -> t
-    | Typ_paren(sk1,t',sk2) -> 
-        { t with term = Typ_paren(sk1, fix_src_t target t', sk2) }
+   (* TODO: perhaps performance improvements *)
+ *)
 
+let minimize_module_prefix (eq_fun : local_env -> local_env -> bool) (env : local_env) (p : Name.t list) : Name.t list =
+begin 
+  let p_env = lookup_env env p in
 
-let rec fix_pat (target : Target.non_ident_target) p = 
-  let old_t = Some(p.typ) in
-  let old_l = p.locn in
-  let trans = fix_pat target in
-    match p.term with
-      | P_as(sk1,p,s,nl,sk2) -> 
-          C.mk_pas old_l sk1 (trans p) s nl sk2 old_t
-      | P_typ(s1,p,s2,t,s3) -> 
-          C.mk_ptyp old_l s1 (trans p) s2 (fix_src_t target t) s3 old_t
-      | P_const(c,ps) -> 
-          C.mk_pconst old_l (id_fix_binding target c) (List.map trans ps) old_t
-      | P_record(s1,fieldpats,s2) ->
-          C.mk_precord old_l
-            s1 
-            (Seplist.map 
-               (fun (fid,s1,p) -> (id_fix_binding target fid,s1,trans p))
-               fieldpats)
-            s2
-            old_t
-      | P_tup(s1,ps,s2) -> 
-          C.mk_ptup old_l s1 (Seplist.map trans ps) s2 old_t
-      | P_list(s1,ps,s2) -> 
-          C.mk_plist old_l s1 (Seplist.map trans ps) s2 p.typ
-      | P_vector(s1,ps,s2) ->
-          C.mk_pvector old_l s1 (Seplist.map trans ps) s2 p.typ
-      | P_vectorC(s1,ps,s2) ->
-          C.mk_pvectorc old_l s1 (List.map trans ps) s2 p.typ
-      | P_paren(s1,p,s2) -> 
-          C.mk_pparen old_l s1 (trans p) s2 old_t
-      | P_cons(p1,s,p2) -> 
-          C.mk_pcons old_l (trans p1) s (trans p2) old_t
-      | P_num_add _ -> p
-      | P_var _ | P_var_annot _ | P_lit _ | P_wild _ ->
-          p
+  let compare_prefix p2 = begin
+    let p2_env_opt = lookup_env_opt env p2 in
 
+    match p2_env_opt with
+      | (Some p2_env) -> eq_fun p_env p2_env
+      | _ -> false
+  end in
 
-let rec fix_exp target e = 
-  let trans = fix_exp target in 
-  let transp = fix_pat target in
-  let old_t = Some(exp_to_typ e) in
-  let old_l = exp_to_locn e in
-    match (C.exp_to_term e) with
-      | Fun(s1,ps,s2,e) ->
-          C.mk_fun old_l s1 (List.map transp ps) s2 (trans e) old_t
-      | Function(s1,pes,s2) ->
-          C.mk_function old_l
-            s1 (Seplist.map 
-                  (fun (p,s1,e,l) -> (transp p,s1,trans e,l))
-                  pes)
-            s2
-            old_t