Mlw: type program declarations

src/core/theory.ml

@@ -886,13 +886,6 @@ let tuple_theory = Hint.memo 17 (fun n ->
   let uc = add_data_decl uc [ts, [fs,pl]] in
   close_theory uc)
 
-let unit_theory =
-  let uc = empty_theory (id_fresh "Unit") ["why3";"Unit"] in
-  let ts = create_tysymbol (id_fresh "unit") [] (Some (ty_tuple [])) in
-  let uc = use_export uc (tuple_theory 0) in
-  let uc = add_ty_decl uc ts in
-  close_theory uc
-
 let tuple_theory_name s =
   let l = String.length s in
   if l < 6 then None else

src/mlw/dexpr.ml

@@ -316,15 +316,15 @@ type 'a later = pvsymbol Mstr.t -> register_old -> 'a
 
 type dspec_final = {
   ds_pre     : term list;
-  ds_post    : (vsymbol option * term) list;
-  ds_xpost   : (vsymbol option * term) list Mexn.t;
-  ds_reads   : vsymbol list;
+  ds_post    : (pvsymbol * term) list;
+  ds_xpost   : (pvsymbol * term) list Mexn.t;
+  ds_reads   : pvsymbol list;
   ds_writes  : term list;
   ds_diverge : bool;
   ds_checkrw : bool;
 }
 
-type dspec = ty -> dspec_final
+type dspec = ity -> dspec_final
   (* Computation specification is also parametrized by the result type.
      All vsymbols in the postcondition clauses in the [ds_post] field
      must have this type. All vsymbols in the exceptional postcondition
@@ -714,13 +714,10 @@ let create_assert = to_fmla
 
 let create_invariant pl = List.map to_fmla pl
 
-let create_post ty ql = List.map (fun (v,f) ->
-  let f = to_fmla f in match v with
-    | None -> Ity.create_post (create_vsymbol (id_fresh "result") ty) f
-    | Some v -> Ty.ty_equal_check ty v.vs_ty; Ity.create_post v f) ql
+let create_post ity ql = List.map (fun (v,f) ->
+  ity_equal_check ity v.pv_ity; Ity.create_post v.pv_vs (to_fmla f)) ql
 
-let create_xpost xql =
-  Mexn.mapi (fun xs ql -> create_post (ty_of_ity xs.xs_ity) ql) xql
+let create_xpost xql = Mexn.mapi (fun xs ql -> create_post xs.xs_ity ql) xql
 
 (** User effects *)
 
@@ -746,9 +743,7 @@ let rec effect_of_term t =
   | _ -> quit ()
 
 let effect_of_dspec dsp =
-  let add_read s v = Spv.add (try restore_pv v with Not_found ->
-    Loc.errorm "unsupported effect expression") s in
-  let pvs = List.fold_left add_read Spv.empty dsp.ds_reads in
+  let pvs = Spv.of_list dsp.ds_reads in
   let add_write (l,eff) t = match effect_of_term t with
     | v, {ity_node = Ityreg reg}, fd ->
         let fs = match fd with
@@ -926,16 +921,15 @@ let add_binders env pvl = List.fold_left add_pvsymbol env pvl
 
 let cty_of_spec env bl dsp dity =
   let ity = ity_of_dity dity in
-  let ty = ty_of_ity ity in
   let bl = binders bl in
   let env = add_binders env bl in
   let preold = Mstr.find_opt "'0" env.old in
   let env, old = add_label env "'0" in
-  let dsp = get_later env dsp ty in
+  let dsp = get_later env dsp ity in
   let _, eff = effect_of_dspec dsp in
   let eff = eff_strong eff in
   let p = rebase_pre env preold old dsp.ds_pre in
-  let q = create_post ty dsp.ds_post in
+  let q = create_post ity dsp.ds_post in
   let xq = create_xpost dsp.ds_xpost in
   create_cty bl p q xq (get_oldies old) eff ity
 
@@ -1200,14 +1194,13 @@ and rec_defn uloc env ghost {fds = dfdl} =
 and lambda uloc env pvl dsp dvl de =
   let env = add_binders env pvl in
   let e = expr uloc env de in
-  let ty = ty_of_ity e.e_ity in
   let preold = Mstr.find_opt "'0" env.old in
   let env, old = add_label env "'0" in
-  let dsp = get_later env dsp ty in
+  let dsp = get_later env dsp e.e_ity in
   let dvl = get_later env dvl in
   let dvl = rebase_variant env preold old dvl in
   let p = rebase_pre env preold old dsp.ds_pre in
-  let q = create_post ty dsp.ds_post in
+  let q = create_post e.e_ity dsp.ds_post in
   let xq = create_xpost dsp.ds_xpost in
   c_fun pvl p q xq (get_oldies old) e, dsp, dvl
 

src/mlw/dexpr.mli

@@ -11,7 +11,6 @@
 
 open Stdlib
 open Ident
-open Ty
 open Term
 open Ity
 open Expr
@@ -68,15 +67,15 @@ type 'a later = pvsymbol Mstr.t -> register_old -> 'a
 
 type dspec_final = {
   ds_pre     : term list;
-  ds_post    : (vsymbol option * term) list;
-  ds_xpost   : (vsymbol option * term) list Mexn.t;
-  ds_reads   : vsymbol list;
+  ds_post    : (pvsymbol * term) list;
+  ds_xpost   : (pvsymbol * term) list Mexn.t;
+  ds_reads   : pvsymbol list;
   ds_writes  : term list;
   ds_diverge : bool;
   ds_checkrw : bool;
 }
 
-type dspec = ty -> dspec_final
+type dspec = ity -> dspec_final
   (* Computation specification is also parametrized by the result type.
      All vsymbols in the postcondition clauses in the [ds_post] field
      must have this type. All vsymbols in the exceptional postcondition

src/mlw/expr.ml

@@ -578,7 +578,8 @@ let is_e_false e = match e.e_node with
   | Eexec {c_node = Capp (s,[])} -> rs_equal s rs_false
   | _ -> false
 
-let rs_tuple = Hint.memo 17 (fun n -> rs_of_ls (fs_tuple n))
+let rs_tuple = Hint.memo 17 (fun n ->
+  ignore (its_tuple n); rs_of_ls (fs_tuple n))
 
 let is_rs_tuple rs = rs_equal rs (rs_tuple (List.length rs.rs_cty.cty_args))
 

src/mlw/pdecl.ml

@@ -421,6 +421,18 @@ let known_add_decl kn0 d =
   if Sid.is_empty unk then kn else
     raise (UnknownIdent (Sid.choose unk))
 
+(** {2 Records/algebraics handling} *)
+
+let find_its_defn kn s =
+  match (Mid.find s.its_ts.ts_name kn).pd_node with
+  | PDtype dl ->
+      let rec search = function
+        | d::_ when its_equal s d.itd_its -> d
+        | _::dl -> search dl
+        | [] -> assert false in
+      search dl
+  | _ -> assert false
+
 (** {2 Pretty-printing} *)
 
 open Format

src/mlw/pdecl.mli

@@ -82,6 +82,8 @@ val known_id : known_map -> ident -> unit
 val known_add_decl : known_map -> pdecl -> known_map
 val merge_known : known_map -> known_map -> known_map
 
+val find_its_defn : known_map -> itysymbol -> its_defn
+
 (** {2 Pretty-printing *)
 
 val print_pdecl : Format.formatter -> pdecl -> unit

src/parser/parser.mly

@@ -579,30 +579,24 @@ top_ghost:
 (* Function declarations *)
 
 type_v:
-| arrow_type_v  { $1 }
-| cast          { PTpure $1 }
-
-arrow_type_v:
-| param params tail_type_c  { PTfunc ($1 @ $2, $3) }
-
-tail_type_c:
-| single_spec spec arrow_type_v { $3, spec_union $1 $2 }
-| COLON simple_type_c           { $2 }
+| params cast spec  { ($1, $2, $3) }
 
+(*
 simple_type_c:
 | ty spec { PTpure $1, $2 }
+*)
 
 (* Function definitions *)
 
 rec_defn:
 | top_ghost labels(lident_rich) binders cast? spec EQUAL spec seq_expr
-    { $2, $1, ($3, $4, $8, spec_union $5 $7) }
+    { $2, $1, ($3, $4, spec_union $5 $7, $8) }
 
 fun_defn:
-| binders cast? spec EQUAL spec seq_expr { ($1, $2, $6, spec_union $3 $5) }
+| binders cast? spec EQUAL spec seq_expr { ($1, $2, spec_union $3 $5, $6) }
 
 fun_expr:
-| FUN binders spec ARROW spec seq_expr { ($2, None, $6, spec_union $3 $5) }
+| FUN binders spec ARROW spec seq_expr { ($2, None, spec_union $3 $5, $6) }
 
 (* Program expressions *)
 
@@ -619,12 +613,14 @@ expr_:
 | expr_arg_
     { match $1 with (* break the infix relation chain *)
       | Einfix (l,o,r) -> Einnfix (l,o,r) | d -> d }
+| expr AMPAMP expr
+    { Eand ($1, $3) }
+| expr BARBAR expr
+    { Eor ($1, $3) }
 | NOT expr %prec prec_prefix_op
     { Enot $2 }
 | prefix_op expr %prec prec_prefix_op
     { Eidapp (Qident $1, [$2]) }
-| l = expr ; o = lazy_op ; r = expr
-    { Elazy (l,o,r) }
 | l = expr ; o = infix_op ; r = expr
     { Einfix (l,o,r) }
 | expr_arg located(expr_arg)+ (* FIXME/TODO: "expr expr_arg" *)
@@ -677,9 +673,9 @@ expr_:
 | quote_uident COLON seq_expr
     { Emark ($1, $3) }
 | LOOP loop_annotation seq_expr END
-    { Eloop ($2, $3) }
+    { let inv, var = $2 in Eloop (inv, var, $3) }
 | WHILE seq_expr DO loop_annotation seq_expr DONE
-    { Ewhile ($2, $4, $5) }
+    { let inv, var = $4 in Ewhile ($2, inv, var, $5) }
 | FOR lident EQUAL seq_expr for_direction seq_expr DO invariant* seq_expr DONE
     { Efor ($2, $4, $5, $6, $8, $9) }
 | ABSURD
@@ -690,12 +686,12 @@ expr_:
     { Eraise ($3, Some $4) }
 | TRY seq_expr WITH bar_list1(exn_handler) END
     { Etry ($2, $4) }
-| ANY simple_type_c
-    { Eany $2 }
+| ANY ty spec
+    { Eany ([], $2, $3) }
 | GHOST expr
     { Eghost $2 }
 | ABSTRACT spec seq_expr END
-    { Eabstract($3, $2) }
+    { Eabstract($2, $3) }
 | assertion_kind LEFTBRC term RIGHTBRC
     { Eassert ($1, $3) }
 | label expr %prec prec_named
@@ -741,30 +737,26 @@ expr_sub:
 
 loop_annotation:
 | (* epsilon *)
-    { { loop_invariant = []; loop_variant = [] } }
+    { [], [] }
 | invariant loop_annotation
-    { let a = $2 in { a with loop_invariant = $1 :: a.loop_invariant } }
+    { let inv, var = $2 in $1 :: inv, var }
 | variant loop_annotation
-    { let a = $2 in { a with loop_variant = variant_union $1 a.loop_variant } }
+    { let inv, var = $2 in inv, variant_union $1 var }
 
 exn_handler:
 | uqualid pat_arg? ARROW seq_expr { $1, $2, $4 }
 
 val_expr:
-| tail_type_c { Eany $1 }
-
-%inline lazy_op:
-| AMPAMP  { LazyAnd }
-| BARBAR  { LazyOr }
+| type_v { Eany $1 }
 
 assertion_kind:
-| ASSERT  { Aassert }
-| ASSUME  { Aassume }
-| CHECK   { Acheck }
+| ASSERT  { Expr.Assert }
+| ASSUME  { Expr.Assume }
+| CHECK   { Expr.Check }
 
 for_direction:
-| TO      { To }
-| DOWNTO  { Downto }
+| TO      { Expr.To }
+| DOWNTO  { Expr.DownTo }
 
 (* Specification *)
 

src/parser/ptree.ml

@@ -166,18 +166,7 @@ type use_clone = use * clone_subst list option
 
 (* program files *)
 
-type assertion_kind = Aassert | Aassume | Acheck
-
-type lazy_op = LazyAnd | LazyOr
-
-type variant = term * qualid option
-
-type loop_annotation = {
-  loop_invariant : invariant;
-  loop_variant   : variant list;
-}
-
-type for_direction = To | Downto
+type variant = (term * qualid option) list
 
 type pre = term
 type post = loc * (pattern * term) list
@@ -189,17 +178,11 @@ type spec = {
   sp_xpost   : xpost list;
   sp_reads   : qualid list;
   sp_writes  : term list;
-  sp_variant : variant list;
+  sp_variant : variant;
   sp_checkrw : bool;
   sp_diverge : bool;
 }
 
-type type_v =
-  | PTpure of pty
-  | PTfunc of param list * type_c
-
-and type_c = type_v * spec
-
 type top_ghost = Gnone | Gghost | Glemma
 
 type expr = {
@@ -228,27 +211,30 @@ and expr_desc =
   (* control *)
   | Esequence of expr * expr
   | Eif of expr * expr * expr
-  | Eloop of loop_annotation * expr
-  | Ewhile of expr * loop_annotation * expr
-  | Elazy of expr * lazy_op * expr
+  | Eloop of invariant * variant * expr
+  | Ewhile of expr * invariant * variant * expr
+  | Eand of expr * expr
+  | Eor of expr * expr
   | Enot of expr
   | Ematch of expr * (pattern * expr) list
   | Eabsurd
   | Eraise of qualid * expr option
   | Etry of expr * (qualid * pattern option * expr) list
-  | Efor of ident * expr * for_direction * expr * invariant * expr
+  | Efor of ident * expr * Expr.for_direction * expr * invariant * expr
   (* annotations *)
-  | Eassert of assertion_kind * term
+  | Eassert of Expr.assertion_kind * term
   | Emark of ident * expr
   | Ecast of expr * pty
-  | Eany of type_c
+  | Eany of any
   | Eghost of expr
-  | Eabstract of expr * spec
+  | Eabstract of spec * expr
   | Enamed of label * expr
 
 and fundef = ident * top_ghost * lambda
 
-and lambda = binder list * pty option * expr * spec
+and lambda = binder list * pty option * spec * expr
+
+and any = param list * pty * spec
 
 type decl =
   | Dtype of type_decl list
@@ -256,7 +242,7 @@ type decl =
   | Dind of Decl.ind_sign * ind_decl list
   | Dprop of Decl.prop_kind * ident * term
   | Dmeta of ident * metarg list
-  | Dval of ident * top_ghost * type_v
+  | Dval of ident * top_ghost * any
   | Dlet of ident * top_ghost * expr
   | Dfun of ident * top_ghost * lambda
   | Drec of fundef list