From 63e2651a4503b6b7d2ea956bba5b35a69b9dfcd5 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Sat, 20 Apr 2024 17:53:12 +0200 Subject: [PATCH] WIP changes --- minuska-examples/m/imp.m | 6 ++++-- minuska/bin/main.ml | 14 ++++++++++---- minuska/lib/micoqprint.ml | 25 +++++++++++++++---------- minuska/lib/minuska_extraction.v | 15 ++++++++++++++- minuska/theories/default_everything.v | 12 +++++++++--- 5 files changed, 52 insertions(+), 20 deletions(-) diff --git a/minuska-examples/m/imp.m b/minuska-examples/m/imp.m index 8bd6011a..c09f3ef5 100644 --- a/minuska-examples/m/imp.m +++ b/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() ; diff --git a/minuska/bin/main.ml b/minuska/bin/main.ml index 5e8d4788..1ff9e8b9 100644 --- a/minuska/bin/main.ml +++ b/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. + *) |} ; () diff --git a/minuska/lib/micoqprint.ml b/minuska/lib/micoqprint.ml index 778b01aa..036d437d 100644 --- a/minuska/lib/micoqprint.ml +++ b/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"; diff --git a/minuska/lib/minuska_extraction.v b/minuska/lib/minuska_extraction.v index 29ea8e46..9ee02d20 100644 --- a/minuska/lib/minuska_extraction.v +++ b/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 *) . \ No newline at end of file diff --git a/minuska/theories/default_everything.v b/minuska/theories/default_everything.v index 6b65958a..4e30ada4 100644 --- a/minuska/theories/default_everything.v +++ b/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. \ No newline at end of file