WIP changes

minuska-examples/m/imp.m

@@ -5,7 +5,7 @@
    z.is(X),                            bool.or(
    bool.is(X),                         bool.or(
    term.same_symbol(X, [unitValue[]]), 
-   bool.false()
+   string.is(X)
 )))) ;
 @context(HOLE): c[HOLE, STATE];
 @strictness: [
@@ -26,7 +26,9 @@
 @rule/simple [aexpr.plus]: plus[X,Y] => z.plus(X, Y) where bool.and(z.is(X), z.is(Y)) ;
 @rule/simple [aexpr.minus]: minus[X,Y] => z.minus(X, Y) where bool.and(z.is(X), z.is(Y)) ;
 
-@rule [var.assign]: c[builtin.cseq[assign[X,V],REST], STATE] => c[builtin.cseq[unitValue[], REST], map.update(STATE, X, V)] where bool.and(term.same_symbol(X, [var[]]), z.is(V)) ;
+@rule [var.assign]: c[builtin.cseq[assign[X,V],REST], STATE]
+  => c[builtin.cseq[unitValue[], REST], map.update(STATE, X, V)]
+   where bool.and(term.same_symbol(X, [var[]]), bool.or(z.is(V), string.is(V))) ;
 @rule [var.lookup]: c[builtin.cseq[X, REST], STATE] => c[builtin.cseq[map.lookup(STATE, X), REST], STATE] where term.same_symbol(X, [var[]]) ;
 
 @rule/simple [stmt.seq]: seq[unitValue[], X] => X where bool.true() ;

minuska/bin/main.ml

@@ -19,26 +19,32 @@ let append_definition input_filename output_channel =
   parse_and_print lexbuf output_channel;
   In_channel.close inx;
   fprintf output_channel "%s\n" {|Definition T := Eval vm_compute in (to_theory Act (process_declarations Act default_act Lang_Decls)). |};
-  fprintf output_channel "%s\n" {|Definition lang_interpreter : StepT := naive_interpreter (fst T).|};
+  fprintf output_channel "%s\n" {|Definition lang_interpreter : StepT := global_naive_interpreter (fst T).|};
   fprintf output_channel "%s\n" {|
-
+    (* This lemma asserts well-formedness of the definition *)
+    Lemma language_well_formed: isSome(RewritingTheory2_wf_heuristics (fst T)).
+    Proof.
+      (* This is the main syntactic check. If this fails, the semantics contain a bad rule. *) ltac1:(compute_done).
+    Qed.
     (* This lemma asserts soundness of the generated interpreter. *)
+    (* Unfortunately, we cannot rely on the extraction here.
     Lemma interp_sound:
         Interpreter_sound'
         (fst T)
         lang_interpreter
     .
     Proof.
-        apply @naive_interpreter_sound.
+        apply @global_naive_interpreter_sound.
         { apply _. }
         ltac1:(assert(Htmp: isSome(RewritingTheory2_wf_heuristics (fst T)))).
         {
-            (* This is the main syntactic check. If this fails, the semantics contain a bad rule. *) ltac1:(compute_done).
+            apply language_well_formed.
         }
         unfold is_true, isSome in Htmp.
         destruct (RewritingTheory2_wf_heuristics (fst T)) eqn:Heq>[|inversion Htmp].
         assumption.
     Qed.
+    *)
   |} ;
   ()
 

minuska/lib/micoqprint.ml

@@ -16,6 +16,7 @@ let builtins_alist =
     "z.eq", "b_eq";
     "z.le", "b_Z_isLe";
     "z.lt", "b_Z_isLt";
+    "string.is", "b_isString";
     "map.hasKey", "b_map_hasKey";
     "map.lookup", "b_map_lookup";
     "map.size", "b_map_size";
@@ -40,19 +41,22 @@ Require Import
   Coq.extraction.ExtrOcamlZInt
   Coq.extraction.ExtrOcamlNatInt
 .
+(*
 From Minuska Require Import
     prelude
     spec
-    string_variables
+    (*string_variables
     BuiltinValue
-    builtins
-    default_static_model
-    naive_interpreter
+    builtins*)
+    (*default_static_model*)
+    (*naive_interpreter*)
     frontend
-    default_everything
     spec_interpreter
     interpreter_results
 .
+*)
+Require Import Minuska.default_everything.
+Existing Instance default_everything.DSM.
 |}
 
 let output_part_2 = {delimiter|
@@ -69,7 +73,8 @@ Instance LangDefaults : Defaults := {|
 
 let builtin2str b =
   match b with
-  | `BuiltinInt n -> "(bv_Z " ^ (string_of_int n) ^ ")"
+  | `BuiltinInt n -> "((*default_everything.*)bv_Z " ^ (string_of_int n) ^ ")"
+  | `BuiltinString s -> "((*default_everything.*)bv_str \"" ^ s ^ "\")"
   | _ -> failwith "Unsupported builtin value (for printing into Coq)"
 
 let rec print_groundterm (oux : Out_channel.t) (g : Syntax.groundterm) : unit =
@@ -143,7 +148,7 @@ let rec print_expr_w_hole (oux : Out_channel.t) (e : Syntax.expr) (hole : string
     match name0 with
     | None -> failwith (String.append "Unknown builtin: " s)
     | Some name1 ->
-        let name = (String.append "default_builtin." name1) in
+        let name = (String.append "(*default_everything.*)" name1) in
         match List.length es with
         | 0 -> fprintf oux "(e_nullary %s)" name
         | 1 ->
@@ -186,9 +191,9 @@ let print_rule (oux : Out_channel.t) (r : Syntax.rule) : unit =
     (
       match (r.frame) with
       | None -> 
-        fprintf oux "basic_rule \"%s\" " (r.name)
+        fprintf oux "(*default_everything.*)basic_rule \"%s\" " (r.name)
       | Some (`Id s) ->
-        fprintf oux "framed_rule frame_%s \"%s\" " s (r.name)
+        fprintf oux "(*default_everything.*)framed_rule frame_%s \"%s\" " s (r.name)
     );
 
     print_pattern oux (r.lhs);
@@ -236,7 +241,7 @@ let print_definition def oux =
     List.iter ~f:(fun fr -> print_frame oux fr) (def.frames);
     (* fprintf oux "%s\n" {|
     Definition basic_rule (name : string) (l : TermOver BuiltinOrVar) (r : TermOver Expression2) (cond : Expression2) : Declaration :=
-      (decl_rule (@mkRuleDeclaration DSM Act name (@mkRewritingRule2 DSM Act l r [(mkSideCondition2 _ (e_nullary default_builtin.b_true) cond)] default_act)))
+      (decl_rule (@mkRuleDeclaration DSM Act name (@mkRewritingRule2 DSM Act l r [(mkSideCondition2 _ (e_nullary b_true) cond)] default_act)))
     .
     |}; *)
     fprintf oux "Definition Lang_Decls : list Declaration := [\n";

minuska/lib/minuska_extraction.v

@@ -8,7 +8,7 @@ Require Export
 .
 From Coq Require Import String Bool Arith ZArith List.
 
-From Minuska Require Import
+From Minuska Require Export
     prelude
     default_everything
 .
@@ -17,9 +17,22 @@ From Minuska Require Import
 Extraction
     "Dsm.ml"
     default_everything.myBuiltinType
+    default_everything.dmyBuiltin
     default_everything.myBuiltin
     default_everything.DSM
     default_everything.GT
     default_everything.gt_term
     default_everything.gt_over
+    default_everything.global_naive_interpreter
+    (*
+      Error:
+The informative inductive type prod has a Prop instance
+in naive_interpreter.naive_interpreter_sound (or in its mutual block).
+This happens when a sort-polymorphic singleton inductive type
+has logical parameters, such as (I,I) : (True * True) : Prop.
+Extraction cannot handle this situation yet.
+Instead, use a sort-monomorphic type such as (True /\ True)
+or extract to Haskell.
+    *)
+    (* default_everything.global_naive_interpreter_sound *)
 .

minuska/theories/default_everything.v

@@ -1,10 +1,12 @@
-From Minuska Require Import
+From Minuska Require Export
     prelude
     spec
     string_variables
     default_static_model
     frontend
-    properties    
+    properties
+    naive_interpreter
+    interpreter_results
 .
 
 Require Minuska.BuiltinValue Minuska.builtins.
@@ -19,7 +21,9 @@ Proof.
 Defined.
 
 Definition myBuiltinType : Type := @BuiltinValue.BuiltinValue0 string.
-Definition myBuiltin := builtins.default_builtin.β.
+Module dmyBuiltin := builtins.default_builtin.
+Export dmyBuiltin.
+Definition myBuiltin := dmyBuiltin.β.
 
 #[export]
 Instance DSM : StaticModel :=
@@ -70,3 +74,5 @@ Definition framed_rule
         [(mkSideCondition2 _ (e_nullary builtins.default_builtin.b_true) cond)] default_act)))
 .
 
+Definition global_naive_interpreter := @naive_interpreter DSM Act.
+Definition global_naive_interpreter_sound := @naive_interpreter_sound DSM Act.